# Documentation

Mathlib.Algebra.GroupWithZero.Units.Basic

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

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.

Instances For
@[simp]
theorem Units.mk0_one {G₀ : Type u_3} [] (h : optParam (1 0) (_ : 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, p g) g hg, 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 hg, p g hg) g, p g (_ : g 0)

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} [] {x : G₀} :
(u, u = x) x 0
theorem GroupWithZero.eq_zero_or_unit {G₀ : Type u_3} [] (a : G₀) :
a = 0 u, a = u
theorem IsUnit.mk0 {G₀ : Type u_3} [] (x : G₀) (hx : x 0) :
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 GroupWithZero.noZeroDivisors {G₀ : Type u_3} [] :
@[simp]
theorem Units.mk0_mul {G₀ : Type u_3} [] (x : G₀) (y : G₀) (hxy : x * y 0) :
Units.mk0 (x * y) hxy = Units.mk0 x (_ : x 0) * Units.mk0 y (_ : y 0)
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
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
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.

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.

Instances For