# Lemmas about units in a `MonoidWithZero` or a `GroupWithZero`. #

We also define `Ring.inverse`, a globally defined function on any ring (in fact any `MonoidWithZero`), which inverts units and sends non-units to zero.

source
@[simp]
theorem Units.ne_zero {M₀ : Type u_2} [MonoidWithZero M₀] [Nontrivial M₀] (u : M₀ ˣ) :
↑u ≠ 0

An element of the unit group of a nonzero monoid with zero represented as an element of the monoid is nonzero.

source
@[simp]
theorem Units.mul_left_eq_zero {M₀ : Type u_2} [MonoidWithZero M₀] (u : M₀ ˣ) {a : M₀} :
a * ↑u = 0 ↔ a = 0
source
@[simp]
theorem Units.mul_right_eq_zero {M₀ : Type u_2} [MonoidWithZero M₀] (u : M₀ ˣ) {a : M₀} :
↑u * a = 0 ↔ a = 0
source
theorem IsUnit.ne_zero {M₀ : Type u_2} [MonoidWithZero M₀] [Nontrivial M₀] {a : M₀} (ha : IsUnit a) :
a ≠ 0
source
theorem IsUnit.mul_right_eq_zero {M₀ : Type u_2} [MonoidWithZero M₀] {a b : M₀} (ha : IsUnit a) :
a * b = 0 ↔ b = 0
source
theorem IsUnit.mul_left_eq_zero {M₀ : Type u_2} [MonoidWithZero M₀] {a b : M₀} (hb : IsUnit b) :
a * b = 0 ↔ a = 0
source
@[simp]
theorem isUnit_zero_iff {M₀ : Type u_2} [MonoidWithZero M₀] :
IsUnit 0 ↔ 0 = 1
source
theorem not_isUnit_zero {M₀ : Type u_2} [MonoidWithZero M₀] [Nontrivial M₀] :
¬IsUnit 0
source
noncomputable def Ring.inverse {M₀ : Type u_2} [MonoidWithZero M₀] :
M₀ → M₀

Introduce a function `inverse` on a monoid with zero `M₀`, which sends `x` to `x⁻¹` if `x` is invertible and to `0` otherwise. This definition is somewhat ad hoc, but one needs a fully (rather than partially) defined inverse function for some purposes, including for calculus.

Note that while this is in the `Ring` namespace for brevity, it requires the weaker assumption `MonoidWithZero M₀` instead of `Ring M₀`.

Equations

- Ring.inverse x = if h : IsUnit x then ↑h.unit⁻¹ else 0

Instances For

source
theorem Ring.inverse_unit {M₀ : Type u_2} [MonoidWithZero M₀] (u : M₀ ˣ) :
inverse ↑u = ↑u⁻¹

By definition, if `x` is invertible then `inverse x = x⁻¹`.

source
theorem Ring.inverse_of_isUnit {M₀ : Type u_2} [MonoidWithZero M₀] {x : M₀} (h : IsUnit x) :
inverse x = ↑h.unit⁻¹
source
@[simp]
theorem Ring.inverse_non_unit {M₀ : Type u_2} [MonoidWithZero M₀] (x : M₀) (h : ¬IsUnit x) :
inverse x = 0

By definition, if `x` is not invertible then `inverse x = 0`.

source
theorem Ring.mul_inverse_cancel {M₀ : Type u_2} [MonoidWithZero M₀] (x : M₀) (h : IsUnit x) :
x * inverse x = 1
source
theorem Ring.inverse_mul_cancel {M₀ : Type u_2} [MonoidWithZero M₀] (x : M₀) (h : IsUnit x) :
inverse x * x = 1
source
theorem Ring.mul_inverse_cancel_right {M₀ : Type u_2} [MonoidWithZero M₀] (x y : M₀) (h : IsUnit x) :
y * x * inverse x = y
source
theorem Ring.inverse_mul_cancel_right {M₀ : Type u_2} [MonoidWithZero M₀] (x y : M₀) (h : IsUnit x) :
y * inverse x * x = y
source
theorem Ring.mul_inverse_cancel_left {M₀ : Type u_2} [MonoidWithZero M₀] (x y : M₀) (h : IsUnit x) :
x * (inverse x * y) = y
source
theorem Ring.inverse_mul_cancel_left {M₀ : Type u_2} [MonoidWithZero M₀] (x y : M₀) (h : IsUnit x) :
inverse x * (x * y) = y
source
theorem Ring.inverse_mul_eq_iff_eq_mul {M₀ : Type u_2} [MonoidWithZero M₀] (x y z : M₀) (h : IsUnit x) :
inverse x * y = z ↔ y = x * z
source
theorem Ring.eq_mul_inverse_iff_mul_eq {M₀ : Type u_2} [MonoidWithZero M₀] (x y z : M₀) (h : IsUnit z) :
x = y * inverse z ↔ x * z = y
source
@[simp]
theorem Ring.inverse_one (M₀ : Type u_2) [MonoidWithZero M₀] :
inverse 1 = 1
source
@[simp]
theorem Ring.inverse_zero (M₀ : Type u_2) [MonoidWithZero M₀] :
inverse 0 = 0
source
theorem IsUnit.ringInverse {M₀ : Type u_2} [MonoidWithZero M₀] {a : M₀} :
IsUnit a → IsUnit (Ring.inverse a)
source
@[deprecated IsUnit.ringInverse (since := "2025-04-22")]
theorem IsUnit.ring_inverse {M₀ : Type u_2} [MonoidWithZero M₀] {a : M₀} :
IsUnit a → IsUnit (Ring.inverse a)

Alias of `IsUnit.ringInverse`.

source
@[deprecated IsUnit.ringInverse (since := "2025-04-22")]
theorem Ring.IsUnit.ringInverse {M₀ : Type u_2} [MonoidWithZero M₀] {a : M₀} :
IsUnit a → IsUnit (inverse a)

Alias of `IsUnit.ringInverse`.

source
@[simp]
theorem isUnit_ringInverse {M₀ : Type u_2} [MonoidWithZero M₀] {a : M₀} :
IsUnit (Ring.inverse a) ↔ IsUnit a
source
@[deprecated isUnit_ringInverse (since := "2025-04-22")]
theorem isUnit_ring_inverse {M₀ : Type u_2} [MonoidWithZero M₀] {a : M₀} :
IsUnit (Ring.inverse a) ↔ IsUnit a

Alias of `isUnit_ringInverse`.

source
def Units.mk0 {G₀ : Type u_3} [GroupWithZero G₀] (a : G₀) (ha : a ≠ 0) :
G₀ ˣ

Embed a non-zero element of a `GroupWithZero` into the unit group. By combining this function with the operations on units, or the `/ₚ` operation, it is possible to write a division as a partial function with three arguments.

Equations

- Units.mk0 a ha = { val := a, inv := a⁻¹, val_inv := ⋯, inv_val := ⋯ }

Instances For

source
@[simp]
theorem Units.mk0_one {G₀ : Type u_3} [GroupWithZero G₀] (h : 1 ≠ 0 := ⋯) :
mk0 1 h = 1
source
@[simp]
theorem Units.val_mk0 {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} (h : a ≠ 0) :
↑(mk0 a h) = a
source
@[simp]
theorem Units.mk0_val {G₀ : Type u_3} [GroupWithZero G₀] (u : G₀ ˣ) (h : ↑u ≠ 0) :
mk0 (↑u) h = u
source
theorem Units.mul_inv' {G₀ : Type u_3} [GroupWithZero G₀] (u : G₀ ˣ) :
↑u * (↑u)⁻¹ = 1
source
theorem Units.inv_mul' {G₀ : Type u_3} [GroupWithZero G₀] (u : G₀ ˣ) :
(↑u)⁻¹ * ↑u = 1
source
@[simp]
theorem Units.mk0_inj {G₀ : Type u_3} [GroupWithZero G₀] {a b : G₀} (ha : a ≠ 0) (hb : b ≠ 0) :
mk0 a ha = mk0 b hb ↔ a = b
source
theorem Units.exists0 {G₀ : Type u_3} [GroupWithZero G₀] {p : G₀ ˣ → Prop} :
(∃ (g : G₀ ˣ), p g) ↔ ∃ (g : G₀), ∃ (hg : g ≠ 0), p (mk0 g hg)

In a group with zero, an existential over a unit can be rewritten in terms of `Units.mk0`.

source
theorem Units.exists0' {G₀ : Type u_3} [GroupWithZero G₀] {p : (g : G₀) → g ≠ 0 → Prop} :
(∃ (g : G₀), ∃ (hg : g ≠ 0), p g hg) ↔ ∃ (g : G₀ ˣ), p ↑g ⋯

An alternative version of `Units.exists0`. This one is useful if Lean cannot figure out `p` when using `Units.exists0` from right to left.

source
@[simp]
theorem Units.exists_iff_ne_zero {G₀ : Type u_3} [GroupWithZero G₀] {p : G₀ → Prop} :
(∃ (u : G₀ ˣ), p ↑u) ↔ ∃ (x : G₀), x ≠ 0 ∧ p x
source
theorem GroupWithZero.eq_zero_or_unit {G₀ : Type u_3} [GroupWithZero G₀] (a : G₀) :
a = 0 ∨ ∃ (u : G₀ ˣ), a = ↑u
source
theorem IsUnit.mk0 {G₀ : Type u_3} [GroupWithZero G₀] (x : G₀) (hx : x ≠ 0) :
IsUnit x
source
@[simp]
theorem isUnit_iff_ne_zero {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} :
IsUnit a ↔ a ≠ 0
source
theorem Ne.isUnit {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} :
a ≠ 0 → IsUnit a

Alias of the reverse direction of `isUnit_iff_ne_zero`.

source
@[instance 10]
instance GroupWithZero.noZeroDivisors {G₀ : Type u_3} [GroupWithZero G₀] :
NoZeroDivisors G₀
source
@[simp]
theorem Units.mk0_mul {G₀ : Type u_3} [GroupWithZero G₀] (x y : G₀) (hxy : x * y ≠ 0) :
mk0 (x * y) hxy = mk0 x ⋯ * mk0 y ⋯
source
theorem div_ne_zero {G₀ : Type u_3} [GroupWithZero G₀] {a b : G₀} (ha : a ≠ 0) (hb : b ≠ 0) :
a / b ≠ 0
source
@[simp]
theorem div_eq_zero_iff {G₀ : Type u_3} [GroupWithZero G₀] {a b : G₀} :
a / b = 0 ↔ a = 0 ∨ b = 0
source
theorem div_ne_zero_iff {G₀ : Type u_3} [GroupWithZero G₀] {a b : G₀} :
a / b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0
source
@[simp]
theorem div_self {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} (h : a ≠ 0) :
a / a = 1
source
theorem eq_mul_inv_iff_mul_eq₀ {G₀ : Type u_3} [GroupWithZero G₀] {a b c : G₀} (hc : c ≠ 0) :
a = b * c⁻¹ ↔ a * c = b
source
theorem eq_inv_mul_iff_mul_eq₀ {G₀ : Type u_3} [GroupWithZero G₀] {a b c : G₀} (hb : b ≠ 0) :
a = b⁻¹ * c ↔ b * a = c
source
theorem inv_mul_eq_iff_eq_mul₀ {G₀ : Type u_3} [GroupWithZero G₀] {a b c : G₀} (ha : a ≠ 0) :
a⁻¹ * b = c ↔ b = a * c
source
theorem mul_inv_eq_iff_eq_mul₀ {G₀ : Type u_3} [GroupWithZero G₀] {a b c : G₀} (hb : b ≠ 0) :
a * b⁻¹ = c ↔ a = c * b
source
theorem mul_inv_eq_one₀ {G₀ : Type u_3} [GroupWithZero G₀] {a b : G₀} (hb : b ≠ 0) :
a * b⁻¹ = 1 ↔ a = b
source
theorem inv_mul_eq_one₀ {G₀ : Type u_3} [GroupWithZero G₀] {a b : G₀} (ha : a ≠ 0) :
a⁻¹ * b = 1 ↔ a = b
source
theorem mul_eq_one_iff_eq_inv₀ {G₀ : Type u_3} [GroupWithZero G₀] {a b : G₀} (hb : b ≠ 0) :
a * b = 1 ↔ a = b⁻¹
source
theorem mul_eq_one_iff_inv_eq₀ {G₀ : Type u_3} [GroupWithZero G₀] {a b : G₀} (ha : a ≠ 0) :
a * b = 1 ↔ a⁻¹ = b
source
theorem mul_eq_of_eq_mul_inv₀ {G₀ : Type u_3} [GroupWithZero G₀] {a b c : G₀} (ha : a ≠ 0) (h : a = c * b⁻¹) :
a * b = c

A variant of `eq_mul_inv_iff_mul_eq₀` that moves the nonzero hypothesis to another variable.

source
theorem mul_eq_of_eq_inv_mul₀ {G₀ : Type u_3} [GroupWithZero G₀] {a b c : G₀} (hb : b ≠ 0) (h : b = a⁻¹ * c) :
a * b = c

A variant of `eq_inv_mul_iff_mul_eq₀` that moves the nonzero hypothesis to another variable.

source
theorem eq_mul_of_inv_mul_eq₀ {G₀ : Type u_3} [GroupWithZero G₀] {a b c : G₀} (hc : c ≠ 0) (h : b⁻¹ * a = c) :
a = b * c

A variant of `inv_mul_eq_iff_eq_mul₀` that moves the nonzero hypothesis to another variable.

source
theorem eq_mul_of_mul_inv_eq₀ {G₀ : Type u_3} [GroupWithZero G₀] {a b c : G₀} (hb : b ≠ 0) (h : a * c⁻¹ = b) :
a = b * c

A variant of `mul_inv_eq_iff_eq_mul₀` that moves the nonzero hypothesis to another variable.

source
theorem div_mul_cancel₀ {G₀ : Type u_3} [GroupWithZero G₀] {b : G₀} (a : G₀) (h : b ≠ 0) :
a / b * b = a
source
theorem mul_one_div_cancel {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} (h : a ≠ 0) :
a * (1 / a) = 1
source
theorem one_div_mul_cancel {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} (h : a ≠ 0) :
1 / a * a = 1
source
@[simp]
theorem div_left_inj' {G₀ : Type u_3} [GroupWithZero G₀] {a b c : G₀} (hc : c ≠ 0) :
a / c = b / c ↔ a = b
source
theorem div_eq_iff {G₀ : Type u_3} [GroupWithZero G₀] {a b c : G₀} (hb : b ≠ 0) :
a / b = c ↔ a = c * b
source
theorem eq_div_iff {G₀ : Type u_3} [GroupWithZero G₀] {a b c : G₀} (hb : b ≠ 0) :
c = a / b ↔ c * b = a
source
theorem div_eq_iff_mul_eq {G₀ : Type u_3} [GroupWithZero G₀] {a b c : G₀} (hb : b ≠ 0) :
a / b = c ↔ c * b = a
source
theorem eq_div_iff_mul_eq {G₀ : Type u_3} [GroupWithZero G₀] {a b c : G₀} (hc : c ≠ 0) :
a = b / c ↔ a * c = b
source
theorem div_eq_of_eq_mul {G₀ : Type u_3} [GroupWithZero G₀] {a b c : G₀} (hb : b ≠ 0) :
a = c * b → a / b = c
source
theorem eq_div_of_mul_eq {G₀ : Type u_3} [GroupWithZero G₀] {a b c : G₀} (hc : c ≠ 0) :
a * c = b → a = b / c
source
theorem div_eq_one_iff_eq {G₀ : Type u_3} [GroupWithZero G₀] {a b : G₀} (hb : b ≠ 0) :
a / b = 1 ↔ a = b
source
theorem div_mul_cancel_right₀ {G₀ : Type u_3} [GroupWithZero G₀] {b : G₀} (hb : b ≠ 0) (a : G₀) :
b / (a * b) = a⁻¹
source
theorem mul_div_mul_right {G₀ : Type u_3} [GroupWithZero G₀] {c : G₀} (a b : G₀) (hc : c ≠ 0) :
a * c / (b * c) = a / b
source
theorem mul_mul_div {G₀ : Type u_3} [GroupWithZero G₀] {b : G₀} (a : G₀) (hb : b ≠ 0) :
a = a * b * (1 / b)
source
theorem div_div_div_cancel_right₀ {G₀ : Type u_3} [GroupWithZero G₀] {c : G₀} (hc : c ≠ 0) (a b : G₀) :
a / c / (b / c) = a / b
source
theorem div_mul_div_cancel₀ {G₀ : Type u_3} [GroupWithZero G₀] {a b c : G₀} (hb : b ≠ 0) :
a / b * (b / c) = a / c
source
theorem div_mul_cancel_of_imp {G₀ : Type u_3} [GroupWithZero G₀] {a b : G₀} (h : b = 0 → a = 0) :
a / b * b = a
source
theorem mul_div_cancel_of_imp {G₀ : Type u_3} [GroupWithZero G₀] {a b : G₀} (h : b = 0 → a = 0) :
a * b / b = a
source
@[simp]
theorem divp_mk0 {G₀ : Type u_3} [GroupWithZero G₀] {b : G₀} (a : G₀) (hb : b ≠ 0) :
a /ₚ Units.mk0 b hb = a / b
source
theorem pow_sub₀ {G₀ : Type u_3} [GroupWithZero G₀] {m n : ℕ} (a : G₀) (ha : a ≠ 0) (h : n ≤ m) :
a ^ (m - n) = a ^ m * (a ^ n)⁻¹
source
theorem pow_sub_of_lt {G₀ : Type u_3} [GroupWithZero G₀] {m n : ℕ} (a : G₀) (h : n < m) :
a ^ (m - n) = a ^ m * (a ^ n)⁻¹
source
theorem inv_pow_sub₀ {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {m n : ℕ} (ha : a ≠ 0) (h : n ≤ m) :
a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
source
theorem inv_pow_sub_of_lt {G₀ : Type u_3} [GroupWithZero G₀] {m n : ℕ} (a : G₀) (h : n < m) :
a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
source
theorem zpow_sub₀ {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} (ha : a ≠ 0) (m n : ℤ) :
a ^ (m - n) = a ^ m / a ^ n
source
theorem zpow_natCast_sub_natCast₀ {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} (ha : a ≠ 0) (m n : ℕ) :
a ^ (↑m - ↑n) = a ^ m / a ^ n
source
theorem zpow_natCast_sub_one₀ {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} (ha : a ≠ 0) (n : ℕ) :
a ^ (↑n - 1) = a ^ n / a
source
theorem zpow_one_sub_natCast₀ {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} (ha : a ≠ 0) (n : ℕ) :
a ^ (1 - ↑n) = a / a ^ n
source
theorem zpow_ne_zero {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} (n : ℤ) :
a ≠ 0 → a ^ n ≠ 0
source
theorem eq_zero_of_zpow_eq_zero {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {n : ℤ} :
a ^ n = 0 → a = 0
source
theorem zpow_eq_zero_iff {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {n : ℤ} (hn : n ≠ 0) :
a ^ n = 0 ↔ a = 0
source
theorem zpow_ne_zero_iff {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} {n : ℤ} (hn : n ≠ 0) :
a ^ n ≠ 0 ↔ a ≠ 0
source
theorem zpow_neg_mul_zpow_self {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} (n : ℤ) (ha : a ≠ 0) :
a ^ (-n) * a ^ n = 1
source
theorem Ring.inverse_eq_inv {G₀ : Type u_3} [GroupWithZero G₀] (a : G₀) :
inverse a = a⁻¹
source
@[simp]
theorem Ring.inverse_eq_inv' {G₀ : Type u_3} [GroupWithZero G₀] :
inverse = Inv.inv
source
@[instance 10]
instance CommGroupWithZero.toCancelCommMonoidWithZero {G₀ : Type u_3} [CommGroupWithZero G₀] :
CancelCommMonoidWithZero G₀
Equations

- One or more equations did not get rendered due to their size.

source
@[instance 100]
instance CommGroupWithZero.toDivisionCommMonoid {G₀ : Type u_3} [CommGroupWithZero G₀] :
DivisionCommMonoid G₀
Equations

- One or more equations did not get rendered due to their size.

source
theorem div_mul_cancel_left₀ {G₀ : Type u_3} [CommGroupWithZero G₀] {a : G₀} (ha : a ≠ 0) (b : G₀) :
a / (a * b) = b⁻¹
source
theorem mul_div_cancel_left_of_imp {G₀ : Type u_3} [CommGroupWithZero G₀] {a b : G₀} (h : a = 0 → b = 0) :
a * b / a = b
source
theorem mul_div_cancel_of_imp' {G₀ : Type u_3} [CommGroupWithZero G₀] {a b : G₀} (h : b = 0 → a = 0) :
b * (a / b) = a
source
theorem mul_div_cancel₀ {G₀ : Type u_3} [CommGroupWithZero G₀] {b : G₀} (a : G₀) (hb : b ≠ 0) :
b * (a / b) = a
source
theorem mul_div_mul_left {G₀ : Type u_3} [CommGroupWithZero G₀] {c : G₀} (a b : G₀) (hc : c ≠ 0) :
c * a / (c * b) = a / b
source
theorem mul_eq_mul_of_div_eq_div {G₀ : Type u_3} [CommGroupWithZero G₀] {b d : G₀} (a c : G₀) (hb : b ≠ 0) (hd : d ≠ 0) (h : a / b = c / d) :
a * d = c * b
source
theorem div_eq_div_iff {G₀ : Type u_3} [CommGroupWithZero G₀] {a b c d : G₀} (hb : b ≠ 0) (hd : d ≠ 0) :
a / b = c / d ↔ a * d = c * b
source
theorem mul_inv_eq_mul_inv_iff {G₀ : Type u_3} [CommGroupWithZero G₀] {a b c d : G₀} (hb : b ≠ 0) (hd : d ≠ 0) :
a * b⁻¹ = c * d⁻¹ ↔ a * d = c * b
source
theorem inv_mul_eq_inv_mul_iff {G₀ : Type u_3} [CommGroupWithZero G₀] {a b c d : G₀} (hb : b ≠ 0) (hd : d ≠ 0) :
b⁻¹ * a = d⁻¹ * c ↔ a * d = c * b
source
theorem div_eq_div_iff_div_eq_div' {G₀ : Type u_3} [CommGroupWithZero G₀] {a b c d : G₀} (hb : b ≠ 0) (hc : c ≠ 0) :
a / b = c / d ↔ a / c = b / d

The `CommGroupWithZero` version of `div_eq_div_iff_div_eq_div`.

source
theorem div_eq_div_of_div_eq_div {G₀ : Type u_3} [CommGroupWithZero G₀] {a b c d : G₀} (hc : c ≠ 0) (hd : d ≠ 0) (h : a / b = c / d) :
a / c = b / d
source
@[simp]
theorem div_div_cancel₀ {G₀ : Type u_3} [CommGroupWithZero G₀] {a b : G₀} (ha : a ≠ 0) :
a / (a / b) = b
source
theorem div_div_cancel_left' {G₀ : Type u_3} [CommGroupWithZero G₀] {a b : G₀} (ha : a ≠ 0) :
a / b / a = b⁻¹
source
theorem div_helper {G₀ : Type u_3} [CommGroupWithZero G₀] {a : G₀} (b : G₀) (h : a ≠ 0) :
1 / (a * b) * a = 1 / b
source
theorem div_div_div_cancel_left' {G₀ : Type u_3} [CommGroupWithZero G₀] {c : G₀} (a b : G₀) (hc : c ≠ 0) :
c / a / (c / b) = b / a
source
@[simp]
theorem div_mul_div_cancel₀' {G₀ : Type u_3} [CommGroupWithZero G₀] {a : G₀} (ha : a ≠ 0) (b c : G₀) :
a / b * (c / a) = c / b
source
noncomputable def groupWithZeroOfIsUnitOrEqZero {M : Type u_4} [Nontrivial M] [hM : MonoidWithZero M] (h : ∀ (a : M), IsUnit a ∨ a = 0) :
GroupWithZero M

Constructs a `GroupWithZero` structure on a `MonoidWithZero` consisting only of units and 0.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
noncomputable def commGroupWithZeroOfIsUnitOrEqZero {M : Type u_4} [Nontrivial M] [hM : CommMonoidWithZero M] (h : ∀ (a : M), IsUnit a ∨ a = 0) :
CommGroupWithZero M

Constructs a `CommGroupWithZero` structure on a `CommMonoidWithZero` consisting only of units and 0.

Equations

- One or more equations did not get rendered due to their size.

Instances For