# 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.

@[simp]
theorem Units.ne_zero {M₀ : Type u_2} [] [] (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.

@[simp]
theorem Units.mul_left_eq_zero {M₀ : Type u_2} [] (u : M₀ˣ) {a : M₀} :
a * u = 0 a = 0
@[simp]
theorem Units.mul_right_eq_zero {M₀ : Type u_2} [] (u : M₀ˣ) {a : M₀} :
u * a = 0 a = 0
theorem IsUnit.ne_zero {M₀ : Type u_2} [] [] {a : M₀} (ha : ) :
a 0
theorem IsUnit.mul_right_eq_zero {M₀ : Type u_2} [] {a : M₀} {b : M₀} (ha : ) :
a * b = 0 b = 0
theorem IsUnit.mul_left_eq_zero {M₀ : Type u_2} [] {a : M₀} {b : M₀} (hb : ) :
a * b = 0 a = 0
@[simp]
theorem isUnit_zero_iff {M₀ : Type u_2} [] :
0 = 1
theorem not_isUnit_zero {M₀ : Type u_2} [] [] :
noncomputable def Ring.inverse {M₀ : Type u_2} [] :
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
• = if h : then h.unit⁻¹ else 0
Instances For
@[simp]
theorem Ring.inverse_unit {M₀ : Type u_2} [] (u : M₀ˣ) :
= u⁻¹

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

@[simp]
theorem Ring.inverse_non_unit {M₀ : Type u_2} [] (x : M₀) (h : ¬) :

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

theorem Ring.mul_inverse_cancel {M₀ : Type u_2} [] (x : M₀) (h : ) :
= 1
theorem Ring.inverse_mul_cancel {M₀ : Type u_2} [] (x : M₀) (h : ) :
= 1
theorem Ring.mul_inverse_cancel_right {M₀ : Type u_2} [] (x : M₀) (y : M₀) (h : ) :
y * x * = y
theorem Ring.inverse_mul_cancel_right {M₀ : Type u_2} [] (x : M₀) (y : M₀) (h : ) :
* x = y
theorem Ring.mul_inverse_cancel_left {M₀ : Type u_2} [] (x : M₀) (y : M₀) (h : ) :
x * () = y
theorem Ring.inverse_mul_cancel_left {M₀ : Type u_2} [] (x : M₀) (y : M₀) (h : ) :
* (x * y) = y
theorem Ring.inverse_mul_eq_iff_eq_mul {M₀ : Type u_2} [] (x : M₀) (y : M₀) (z : M₀) (h : ) :
= z y = x * z
theorem Ring.eq_mul_inverse_iff_mul_eq {M₀ : Type u_2} [] (x : M₀) (y : M₀) (z : M₀) (h : ) :
x = x * z = y
@[simp]
theorem Ring.inverse_one (M₀ : Type u_2) [] :
@[simp]
theorem Ring.inverse_zero (M₀ : Type u_2) [] :
theorem IsUnit.ring_inverse {M₀ : Type u_2} [] {a : M₀} :
@[simp]
theorem isUnit_ring_inverse {M₀ : Type u_2} [] {a : M₀} :
def Units.mk0 {G₀ : Type u_3} [] (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
@[simp]
theorem Units.mk0_one {G₀ : Type u_3} [] (h : optParam (1 0) ) :
= 1
@[simp]
theorem Units.val_mk0 {G₀ : Type u_3} [] {a : G₀} (h : a 0) :
() = a
@[simp]
theorem Units.mk0_val {G₀ : Type u_3} [] (u : G₀ˣ) (h : u 0) :
Units.mk0 (u) h = u
theorem Units.mul_inv' {G₀ : Type u_3} [] (u : G₀ˣ) :
u * (u)⁻¹ = 1
theorem Units.inv_mul' {G₀ : Type u_3} [] (u : G₀ˣ) :
(u)⁻¹ * u = 1
@[simp]
theorem Units.mk0_inj {G₀ : Type u_3} [] {a : G₀} {b : G₀} (ha : a 0) (hb : b 0) :
Units.mk0 a ha = Units.mk0 b hb a = b
theorem Units.exists0 {G₀ : Type u_3} [] {p : G₀ˣProp} :
(∃ (g : G₀ˣ), p g) ∃ (g : G₀), ∃ (hg : g 0), p (Units.mk0 g hg)

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

theorem Units.exists0' {G₀ : Type u_3} [] {p : (g : G₀) → g 0Prop} :
(∃ (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.

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

Alias of the reverse direction of isUnit_iff_ne_zero.

@[instance 10]
instance GroupWithZero.noZeroDivisors {G₀ : Type u_3} [] :
Equations
• =
@[simp]
theorem Units.mk0_mul {G₀ : Type u_3} [] (x : G₀) (y : G₀) (hxy : x * y 0) :
Units.mk0 (x * y) hxy = *
theorem div_ne_zero {G₀ : Type u_3} [] {a : G₀} {b : G₀} (ha : a 0) (hb : b 0) :
a / b 0
@[simp]
theorem div_eq_zero_iff {G₀ : Type u_3} [] {a : G₀} {b : G₀} :
a / b = 0 a = 0 b = 0
theorem div_ne_zero_iff {G₀ : Type u_3} [] {a : G₀} {b : G₀} :
a / b 0 a 0 b 0
@[simp]
theorem div_self {G₀ : Type u_3} [] {a : G₀} (h : a 0) :
a / a = 1
theorem eq_mul_inv_iff_mul_eq₀ {G₀ : Type u_3} [] {a : G₀} {b : G₀} {c : G₀} (hc : c 0) :
a = b * c⁻¹ a * c = b
theorem eq_inv_mul_iff_mul_eq₀ {G₀ : Type u_3} [] {a : G₀} {b : G₀} {c : G₀} (hb : b 0) :
a = b⁻¹ * c b * a = c
theorem inv_mul_eq_iff_eq_mul₀ {G₀ : Type u_3} [] {a : G₀} {b : G₀} {c : G₀} (ha : a 0) :
a⁻¹ * b = c b = a * c
theorem mul_inv_eq_iff_eq_mul₀ {G₀ : Type u_3} [] {a : G₀} {b : G₀} {c : G₀} (hb : b 0) :
a * b⁻¹ = c a = c * b
theorem mul_inv_eq_one₀ {G₀ : Type u_3} [] {a : G₀} {b : G₀} (hb : b 0) :
a * b⁻¹ = 1 a = b
theorem inv_mul_eq_one₀ {G₀ : Type u_3} [] {a : G₀} {b : G₀} (ha : a 0) :
a⁻¹ * b = 1 a = b
theorem mul_eq_one_iff_eq_inv₀ {G₀ : Type u_3} [] {a : G₀} {b : G₀} (hb : b 0) :
a * b = 1 a = b⁻¹
theorem mul_eq_one_iff_inv_eq₀ {G₀ : Type u_3} [] {a : G₀} {b : G₀} (ha : a 0) :
a * b = 1 a⁻¹ = b
theorem mul_eq_of_eq_mul_inv₀ {G₀ : Type u_3} [] {a : G₀} {b : G₀} {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.

theorem mul_eq_of_eq_inv_mul₀ {G₀ : Type u_3} [] {a : G₀} {b : G₀} {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.

theorem eq_mul_of_inv_mul_eq₀ {G₀ : Type u_3} [] {a : G₀} {b : G₀} {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.

theorem eq_mul_of_mul_inv_eq₀ {G₀ : Type u_3} [] {a : G₀} {b : G₀} {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.

@[simp]
theorem div_mul_cancel₀ {G₀ : Type u_3} [] {b : G₀} (a : G₀) (h : b 0) :
a / b * b = a
theorem mul_one_div_cancel {G₀ : Type u_3} [] {a : G₀} (h : a 0) :
a * (1 / a) = 1
theorem one_div_mul_cancel {G₀ : Type u_3} [] {a : G₀} (h : a 0) :
1 / a * a = 1
theorem div_left_inj' {G₀ : Type u_3} [] {a : G₀} {b : G₀} {c : G₀} (hc : c 0) :
a / c = b / c a = b
theorem div_eq_iff {G₀ : Type u_3} [] {a : G₀} {b : G₀} {c : G₀} (hb : b 0) :
a / b = c a = c * b
theorem eq_div_iff {G₀ : Type u_3} [] {a : G₀} {b : G₀} {c : G₀} (hb : b 0) :
c = a / b c * b = a
theorem div_eq_iff_mul_eq {G₀ : Type u_3} [] {a : G₀} {b : G₀} {c : G₀} (hb : b 0) :
a / b = c c * b = a
theorem eq_div_iff_mul_eq {G₀ : Type u_3} [] {a : G₀} {b : G₀} {c : G₀} (hc : c 0) :
a = b / c a * c = b
theorem div_eq_of_eq_mul {G₀ : Type u_3} [] {a : G₀} {b : G₀} {c : G₀} (hb : b 0) :
a = c * ba / b = c
theorem eq_div_of_mul_eq {G₀ : Type u_3} [] {a : G₀} {b : G₀} {c : G₀} (hc : c 0) :
a * c = ba = b / c
theorem div_eq_one_iff_eq {G₀ : Type u_3} [] {a : G₀} {b : G₀} (hb : b 0) :
a / b = 1 a = b
theorem div_mul_cancel_right₀ {G₀ : Type u_3} [] {b : G₀} (hb : b 0) (a : G₀) :
b / (a * b) = a⁻¹
@[deprecated div_mul_cancel_right₀]
theorem div_mul_left {G₀ : Type u_3} [] {a : G₀} {b : G₀} (hb : b 0) :
b / (a * b) = 1 / a
theorem mul_div_mul_right {G₀ : Type u_3} [] {c : G₀} (a : G₀) (b : G₀) (hc : c 0) :
a * c / (b * c) = a / b
theorem mul_mul_div {G₀ : Type u_3} [] {b : G₀} (a : G₀) (hb : b 0) :
a = a * b * (1 / b)
theorem div_div_div_cancel_right {G₀ : Type u_3} [] {b : G₀} {c : G₀} (a : G₀) (hc : c 0) :
a / c / (b / c) = a / b
theorem div_mul_div_cancel {G₀ : Type u_3} [] {b : G₀} {c : G₀} (a : G₀) (hc : c 0) :
a / c * (c / b) = a / b
theorem div_mul_cancel_of_imp {G₀ : Type u_3} [] {a : G₀} {b : G₀} (h : b = 0a = 0) :
a / b * b = a
theorem mul_div_cancel_of_imp {G₀ : Type u_3} [] {a : G₀} {b : G₀} (h : b = 0a = 0) :
a * b / b = a
@[simp]
theorem divp_mk0 {G₀ : Type u_3} [] {b : G₀} (a : G₀) (hb : b 0) :
a /ₚ Units.mk0 b hb = a / b
theorem pow_sub₀ {G₀ : Type u_3} [] {m : } {n : } (a : G₀) (ha : a 0) (h : n m) :
a ^ (m - n) = a ^ m * (a ^ n)⁻¹
theorem pow_sub_of_lt {G₀ : Type u_3} [] {m : } {n : } (a : G₀) (h : n < m) :
a ^ (m - n) = a ^ m * (a ^ n)⁻¹
theorem inv_pow_sub₀ {G₀ : Type u_3} [] {a : G₀} {m : } {n : } (ha : a 0) (h : n m) :
a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
theorem inv_pow_sub_of_lt {G₀ : Type u_3} [] {m : } {n : } (a : G₀) (h : n < m) :
a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
theorem zpow_sub₀ {G₀ : Type u_3} [] {a : G₀} (ha : a 0) (m : ) (n : ) :
a ^ (m - n) = a ^ m / a ^ n
theorem zpow_ne_zero {G₀ : Type u_3} [] {a : G₀} (n : ) :
a 0a ^ n 0
theorem eq_zero_of_zpow_eq_zero {G₀ : Type u_3} [] {a : G₀} {n : } :
a ^ n = 0a = 0
@[deprecated zpow_ne_zero]
theorem zpow_ne_zero_of_ne_zero {G₀ : Type u_3} [] {a : G₀} (n : ) :
a 0a ^ n 0

Alias of zpow_ne_zero.

@[deprecated eq_zero_of_zpow_eq_zero]
theorem zpow_eq_zero {G₀ : Type u_3} [] {a : G₀} {n : } :
a ^ n = 0a = 0

Alias of eq_zero_of_zpow_eq_zero.

theorem zpow_eq_zero_iff {G₀ : Type u_3} [] {a : G₀} {n : } (hn : n 0) :
a ^ n = 0 a = 0
theorem zpow_ne_zero_iff {G₀ : Type u_3} [] {a : G₀} {n : } (hn : n 0) :
a ^ n 0 a 0
theorem zpow_neg_mul_zpow_self {G₀ : Type u_3} [] {a : G₀} (n : ) (ha : a 0) :
a ^ (-n) * a ^ n = 1
theorem Ring.inverse_eq_inv {G₀ : Type u_3} [] (a : G₀) :
@[simp]
theorem Ring.inverse_eq_inv' {G₀ : Type u_3} [] :
Ring.inverse = Inv.inv
@[simp]
theorem unitsEquivNeZero_symm_apply {α : Type u_1} [] (a : { a : α // a 0 }) :
unitsEquivNeZero.symm a = Units.mk0 a
@[simp]
theorem unitsEquivNeZero_apply_coe {α : Type u_1} [] (a : αˣ) :
(unitsEquivNeZero a) = a
def unitsEquivNeZero {α : Type u_1} [] :
αˣ { a : α // a 0 }

In a GroupWithZero α, the unit group αˣ is equivalent to the subtype of nonzero elements.

Equations
• unitsEquivNeZero = { toFun := fun (a : αˣ) => a, , invFun := fun (a : { a : α // a 0 }) => Units.mk0 a , left_inv := , right_inv := }
Instances For
@[instance 10]
Equations
• CommGroupWithZero.toCancelCommMonoidWithZero = let __src := GroupWithZero.toCancelMonoidWithZero; let __src_1 := CommGroupWithZero.toCommMonoidWithZero; CancelCommMonoidWithZero.mk
@[instance 100]
instance CommGroupWithZero.toDivisionCommMonoid {G₀ : Type u_3} [] :
Equations
• CommGroupWithZero.toDivisionCommMonoid = let __spread.0 := inst; let __spread.1 := GroupWithZero.toDivisionMonoid;
theorem div_mul_cancel_left₀ {G₀ : Type u_3} [] {a : G₀} (ha : a 0) (b : G₀) :
a / (a * b) = b⁻¹
@[deprecated div_mul_cancel_left₀]
theorem div_mul_right {G₀ : Type u_3} [] {a : G₀} (b : G₀) (ha : a 0) :
a / (a * b) = 1 / b
theorem mul_div_cancel_left_of_imp {G₀ : Type u_3} [] {a : G₀} {b : G₀} (h : a = 0b = 0) :
a * b / a = b
theorem mul_div_cancel_of_imp' {G₀ : Type u_3} [] {a : G₀} {b : G₀} (h : b = 0a = 0) :
b * (a / b) = a
theorem mul_div_cancel₀ {G₀ : Type u_3} [] {b : G₀} (a : G₀) (hb : b 0) :
b * (a / b) = a
theorem mul_div_mul_left {G₀ : Type u_3} [] {c : G₀} (a : G₀) (b : G₀) (hc : c 0) :
c * a / (c * b) = a / b
theorem mul_eq_mul_of_div_eq_div {G₀ : Type u_3} [] {b : G₀} {d : G₀} (a : G₀) (c : G₀) (hb : b 0) (hd : d 0) (h : a / b = c / d) :
a * d = c * b
theorem div_eq_div_iff {G₀ : Type u_3} [] {a : G₀} {b : G₀} {c : G₀} {d : G₀} (hb : b 0) (hd : d 0) :
a / b = c / d a * d = c * b
theorem div_eq_div_iff_div_eq_div' {G₀ : Type u_3} [] {a : G₀} {b : G₀} {c : G₀} {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.

theorem div_div_cancel' {G₀ : Type u_3} [] {a : G₀} {b : G₀} (ha : a 0) :
a / (a / b) = b
theorem div_div_cancel_left' {G₀ : Type u_3} [] {a : G₀} {b : G₀} (ha : a 0) :
a / b / a = b⁻¹
theorem div_helper {G₀ : Type u_3} [] {a : G₀} (b : G₀) (h : a 0) :
1 / (a * b) * a = 1 / b
theorem div_div_div_cancel_left' {G₀ : Type u_3} [] {c : G₀} (a : G₀) (b : G₀) (hc : c 0) :
c / a / (c / b) = b / a
noncomputable def groupWithZeroOfIsUnitOrEqZero {M : Type u_8} [] [hM : ] (h : ∀ (a : M), a = 0) :

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

Equations
Instances For
noncomputable def commGroupWithZeroOfIsUnitOrEqZero {M : Type u_8} [] [hM : ] (h : ∀ (a : M), a = 0) :

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

Equations
Instances For
@[deprecated mul_div_cancel₀]
theorem mul_div_cancel' {G₀ : Type u_3} [] {b : G₀} (a : G₀) (hb : b 0) :
b * (a / b) = a

Alias of mul_div_cancel₀.