mathlib3 documentation

algebra.group_with_zero.units.basic

Lemmas about units in a monoid_with_zero or a group_with_zero. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source
@[simp]
theorem units.ne_zero {M₀ : Type u_2} [monoid_with_zero 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} [monoid_with_zero M₀] (u : M₀ˣ) {a : M₀} :
a * ↑u = 0 ↔ a = 0
source
@[simp]
theorem units.mul_right_eq_zero {M₀ : Type u_2} [monoid_with_zero M₀] (u : M₀ˣ) {a : M₀} :
↑u * a = 0 ↔ a = 0
source
theorem is_unit.ne_zero {M₀ : Type u_2} [monoid_with_zero M₀] [nontrivial M₀] {a : M₀} (ha : is_unit a) :
a ≠ 0
source
theorem is_unit.mul_right_eq_zero {M₀ : Type u_2} [monoid_with_zero M₀] {a b : M₀} (ha : is_unit a) :
a * b = 0 ↔ b = 0
source
theorem is_unit.mul_left_eq_zero {M₀ : Type u_2} [monoid_with_zero M₀] {a b : M₀} (hb : is_unit b) :
a * b = 0 ↔ a = 0
source
@[simp]
theorem is_unit_zero_iff {M₀ : Type u_2} [monoid_with_zero M₀] :
is_unit 0 ↔ 0 = 1
source
@[simp]
theorem not_is_unit_zero {M₀ : Type u_2} [monoid_with_zero M₀] [nontrivial M₀] :
¬is_unit 0
source
noncomputable def ring.inverse {M₀ : Type u_2} [monoid_with_zero 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 monoid_with_zero M₀ instead of ring M₀.

Equations
source
@[simp]
theorem ring.inverse_unit {M₀ : Type u_2} [monoid_with_zero M₀] (u : M₀ˣ) :
ring.inverse ↑u = ↑u⁻¹

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

source
@[simp]
theorem ring.inverse_non_unit {M₀ : Type u_2} [monoid_with_zero M₀] (x : M₀) (h : ¬is_unit x) :
ring.inverse x = 0

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

source
theorem ring.mul_inverse_cancel {M₀ : Type u_2} [monoid_with_zero M₀] (x : M₀) (h : is_unit x) :
x * ring.inverse x = 1
source
theorem ring.inverse_mul_cancel {M₀ : Type u_2} [monoid_with_zero M₀] (x : M₀) (h : is_unit x) :
ring.inverse x * x = 1
source
theorem ring.mul_inverse_cancel_right {M₀ : Type u_2} [monoid_with_zero M₀] (x y : M₀) (h : is_unit x) :
y * x * ring.inverse x = y
source
theorem ring.inverse_mul_cancel_right {M₀ : Type u_2} [monoid_with_zero M₀] (x y : M₀) (h : is_unit x) :
y * ring.inverse x * x = y
source
theorem ring.mul_inverse_cancel_left {M₀ : Type u_2} [monoid_with_zero M₀] (x y : M₀) (h : is_unit x) :
x * (ring.inverse x * y) = y
source
theorem ring.inverse_mul_cancel_left {M₀ : Type u_2} [monoid_with_zero M₀] (x y : M₀) (h : is_unit x) :
ring.inverse x * (x * y) = y
source
theorem ring.inverse_mul_eq_iff_eq_mul {M₀ : Type u_2} [monoid_with_zero M₀] (x y z : M₀) (h : is_unit x) :
ring.inverse x * y = z ↔ y = x * z
source
theorem ring.eq_mul_inverse_iff_mul_eq {M₀ : Type u_2} [monoid_with_zero M₀] (x y z : M₀) (h : is_unit z) :
x = y * ring.inverse z ↔ x * z = y
source
@[simp]
theorem ring.inverse_one (M₀ : Type u_2) [monoid_with_zero M₀] :
ring.inverse 1 = 1
source
@[simp]
theorem ring.inverse_zero (M₀ : Type u_2) [monoid_with_zero M₀] :
ring.inverse 0 = 0
source
theorem is_unit.ring_inverse {M₀ : Type u_2} [monoid_with_zero M₀] {a : M₀} :
is_unit a → is_unit (ring.inverse a)
source
@[simp]
theorem is_unit_ring_inverse {M₀ : Type u_2} [monoid_with_zero M₀] {a : M₀} :
is_unit (ring.inverse a) ↔ is_unit a
source
def units.mk0 {G₀ : Type u_3} [group_with_zero G₀] (a : G₀) (ha : a ≠ 0) :
G₀ˣ

Embed a non-zero element of a group_with_zero 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
source
@[simp]
theorem units.mk0_one {G₀ : Type u_3} [group_with_zero G₀] (h : 1 ≠ 0 := one_ne_zero) :
units.mk0 1 h = 1
source
@[simp]
theorem units.coe_mk0 {G₀ : Type u_3} [group_with_zero G₀] {a : G₀} (h : a ≠ 0) :
↑(units.mk0 a h) = a
source
@[simp]
theorem units.mk0_coe {G₀ : Type u_3} [group_with_zero G₀] (u : G₀ˣ) (h : ↑u ≠ 0) :
units.mk0 ↑u h = u
source
@[simp]
theorem units.mul_inv' {G₀ : Type u_3} [group_with_zero G₀] (u : G₀ˣ) :
↑u * (↑u)⁻¹ = 1
source
@[simp]
theorem units.inv_mul' {G₀ : Type u_3} [group_with_zero G₀] (u : G₀ˣ) :
(↑u)⁻¹ * ↑u = 1
source
@[simp]
theorem units.mk0_inj {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} (ha : a ≠ 0) (hb : b ≠ 0) :
units.mk0 a ha = units.mk0 b hb ↔ a = b
source
theorem units.exists0 {G₀ : Type u_3} [group_with_zero G₀] {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.

source
theorem units.exists0' {G₀ : Type u_3} [group_with_zero 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} [group_with_zero G₀] {x : G₀} :
(∃ (u : G₀ˣ), ↑u = x) ↔ x ≠ 0
source
theorem group_with_zero.eq_zero_or_unit {G₀ : Type u_3} [group_with_zero G₀] (a : G₀) :
a = 0 ∨ ∃ (u : G₀ˣ), a = ↑u
source
theorem is_unit.mk0 {G₀ : Type u_3} [group_with_zero G₀] (x : G₀) (hx : x ≠ 0) :
is_unit x
source
theorem is_unit_iff_ne_zero {G₀ : Type u_3} [group_with_zero G₀] {a : G₀} :
is_unit a ↔ a ≠ 0
source
@[protected]
theorem ne.is_unit {G₀ : Type u_3} [group_with_zero G₀] {a : G₀} :
a ≠ 0 → is_unit a

Alias of the reverse direction of is_unit_iff_ne_zero.

source
@[protected, instance]
def group_with_zero.no_zero_divisors {G₀ : Type u_3} [group_with_zero G₀] :
no_zero_divisors G₀
source
@[simp]
theorem units.mk0_mul {G₀ : Type u_3} [group_with_zero G₀] (x y : G₀) (hxy : x * y ≠ 0) :
units.mk0 (x * y) hxy = units.mk0 x _ * units.mk0 y _
source
theorem div_ne_zero {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} (ha : a ≠ 0) (hb : b ≠ 0) :
a / b ≠ 0
source
@[simp]
theorem div_eq_zero_iff {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} :
a / b = 0 ↔ a = 0 ∨ b = 0
source
theorem div_ne_zero_iff {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} :
a / b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0
source
theorem ring.inverse_eq_inv {G₀ : Type u_3} [group_with_zero G₀] (a : G₀) :
ring.inverse a = a⁻¹
source
@[simp]
theorem ring.inverse_eq_inv' {G₀ : Type u_3} [group_with_zero G₀] :
ring.inverse = has_inv.inv
source
@[protected, instance]
def comm_group_with_zero.to_cancel_comm_monoid_with_zero {G₀ : Type u_3} [comm_group_with_zero G₀] :
cancel_comm_monoid_with_zero G₀
Equations
source
@[protected, instance]
def comm_group_with_zero.to_division_comm_monoid {G₀ : Type u_3} [comm_group_with_zero G₀] :
division_comm_monoid G₀
Equations
source
noncomputable def group_with_zero_of_is_unit_or_eq_zero {M : Type u_8} [nontrivial M] [hM : monoid_with_zero M] (h : ∀ (a : M), is_unit a ∨ a = 0) :
group_with_zero M

Constructs a group_with_zero structure on a monoid_with_zero consisting only of units and 0.

Equations
source
noncomputable def comm_group_with_zero_of_is_unit_or_eq_zero {M : Type u_8} [nontrivial M] [hM : comm_monoid_with_zero M] (h : ∀ (a : M), is_unit a ∨ a = 0) :
comm_group_with_zero M

Constructs a comm_group_with_zero structure on a comm_monoid_with_zero consisting only of units and 0.

Equations