Groups with an adjoined zero element

This file describes structures that are not usually studied on their own right in mathematics, namely a special sort of monoid: apart from a distinguished “zero element” they form a group, or in other words, they are groups with an adjoined zero element.

Examples are:

• division rings;
• the value monoid of a multiplicative valuation;
• in particular, the non-negative real numbers.

Main definitions

Various lemmas about GroupWithZero and CommGroupWithZero. To reduce import dependencies, the type-classes themselves are in Algebra.GroupWithZero.Defs.

Implementation details

As is usual in mathlib, we extend the inverse function to the zero element, and require 0⁻¹ = 0.

theorem left_ne_zero_of_mul {M₀ : Type u_1} [MulZeroClass M₀] {a b : M₀} : a * b ≠ 0 → a ≠ 0

theorem right_ne_zero_of_mul {M₀ : Type u_1} [MulZeroClass M₀] {a b : M₀} : a * b ≠ 0 → b ≠ 0

theorem ne_zero_and_ne_zero_of_mul {M₀ : Type u_1} [MulZeroClass M₀] {a b : M₀} (h : a * b ≠ 0) : a ≠ 0 ∧ b ≠ 0

theorem mul_eq_zero_of_ne_zero_imp_eq_zero {M₀ : Type u_1} [MulZeroClass M₀] {a b : M₀} (h : a ≠ 0 → b = 0) : a * b = 0

theorem zero_mul_eq_const {M₀ : Type u_1} [MulZeroClass M₀] : (fun (x : M₀) => 0 * x) = Function.const M₀ 0

To match one_mul_eq_id.

theorem mul_zero_eq_const {M₀ : Type u_1} [MulZeroClass M₀] : (fun (x : M₀) => x * 0) = Function.const M₀ 0

To match mul_one_eq_id.

theorem eq_zero_of_mul_self_eq_zero {M₀ : Type u_1} [Mul M₀] [Zero M₀] [NoZeroDivisors M₀] {a : M₀} (h : a * a = 0) : a = 0

theorem mul_ne_zero {M₀ : Type u_1} [Mul M₀] [Zero M₀] [NoZeroDivisors M₀] {a b : M₀} (ha : a ≠ 0) (hb : b ≠ 0) : a * b ≠ 0

instance NeZero.mul {M₀ : Type u_1} [Zero M₀] [Mul M₀] [NoZeroDivisors M₀] {x y : M₀} [NeZero x] [NeZero y] : NeZero (x * y)

theorem eq_zero_of_zero_eq_one {M₀ : Type u_1} [MulZeroOneClass M₀] (h : 0 = 1) (a : M₀) : a = 0

In a monoid with zero, if zero equals one, then zero is the only element.

def uniqueOfZeroEqOne {M₀ : Type u_1} [MulZeroOneClass M₀] (h : 0 = 1) : Unique M₀

In a monoid with zero, if zero equals one, then zero is the unique element.

Somewhat arbitrarily, we define the default element to be 0. All other elements will be provably equal to it, but not necessarily definitionally equal.

Equations

• uniqueOfZeroEqOne h = { default := 0, uniq := ⋯ }

theorem subsingleton_iff_zero_eq_one {M₀ : Type u_1} [MulZeroOneClass M₀] : 0 = 1 ↔ Subsingleton M₀

In a monoid with zero, zero equals one if and only if all elements of that semiring are equal.

theorem subsingleton_of_zero_eq_one {M₀ : Type u_1} [MulZeroOneClass M₀] : 0 = 1 → Subsingleton M₀

Alias of the forward direction of subsingleton_iff_zero_eq_one.

---

In a monoid with zero, zero equals one if and only if all elements of that semiring are equal.

theorem eq_of_zero_eq_one {M₀ : Type u_1} [MulZeroOneClass M₀] (h : 0 = 1) (a b : M₀) : a = b

theorem zero_ne_one_or_forall_eq_0 {M₀ : Type u_1} [MulZeroOneClass M₀] : 0 ≠ 1 ∨ ∀ (a : M₀), a = 0

In a monoid with zero, either zero and one are nonequal, or zero is the only element.

theorem left_ne_zero_of_mul_eq_one {M₀ : Type u_1} [MulZeroOneClass M₀] [Nontrivial M₀] {a b : M₀} (h : a * b = 1) : a ≠ 0

theorem right_ne_zero_of_mul_eq_one {M₀ : Type u_1} [MulZeroOneClass M₀] [Nontrivial M₀] {a b : M₀} (h : a * b = 1) : b ≠ 0

def IsNilpotent {R : Type u_3} [Zero R] [Pow R ℕ] (x : R) : Prop

An element is said to be nilpotent if some natural-number-power of it equals zero.

Note that we require only the bare minimum assumptions for the definition to make sense. Even MonoidWithZero is too strong since nilpotency is important in the study of rings that are only power-associative.

Equations

• IsNilpotent x = ∃ (n : ℕ), x ^ n = 0

theorem IsNilpotent.mk {R : Type u_3} [Zero R] [Pow R ℕ] (x : R) (n : ℕ) (e : x ^ n = 0) : IsNilpotent x

@[simp]

theorem isNilpotent_of_subsingleton {R : Type u_3} {x : R} [Zero R] [Pow R ℕ] [Subsingleton R] : IsNilpotent x

@[simp]

theorem IsNilpotent.zero {R : Type u_3} [MonoidWithZero R] : IsNilpotent 0

theorem not_isNilpotent_one {R : Type u_3} [MonoidWithZero R] [Nontrivial R] : ¬IsNilpotent 1

theorem IsNilpotent.pow_succ (n : ℕ) {S : Type u_5} [MonoidWithZero S] {x : S} (hx : IsNilpotent x) : IsNilpotent (x ^ n.succ)

theorem IsNilpotent.of_pow {R : Type u_3} [MonoidWithZero R] {x : R} {m : ℕ} (h : IsNilpotent (x ^ m)) : IsNilpotent x

theorem IsNilpotent.pow_of_pos {n : ℕ} {S : Type u_5} [MonoidWithZero S] {x : S} (hx : IsNilpotent x) (hn : n ≠ 0) : IsNilpotent (x ^ n)

@[simp]

theorem IsNilpotent.pow_iff_pos {n : ℕ} {S : Type u_5} [MonoidWithZero S] {x : S} (hn : n ≠ 0) : IsNilpotent (x ^ n) ↔ IsNilpotent x

class IsReduced (R : Type u_5) [Zero R] [Pow R ℕ] : Prop

A structure that has zero and pow is reduced if it has no nonzero nilpotent elements.

• eq_zero (x : R) : IsNilpotent x → x = 0

  A reduced structure has no nonzero nilpotent elements.

theorem isReduced_iff (R : Type u_5) [Zero R] [Pow R ℕ] : IsReduced R ↔ ∀ (x : R), IsNilpotent x → x = 0

theorem eq_zero_of_pow_eq_zero {R : Type u_3} {x : R} [Zero R] [Pow R ℕ] [IsReduced R] {n : ℕ} (h : x ^ n = 0) : x = 0

@[instance 900]

instance isReduced_of_subsingleton {R : Type u_3} [Zero R] [Pow R ℕ] [Subsingleton R] : IsReduced R

theorem IsNilpotent.eq_zero {R : Type u_3} {x : R} [Zero R] [Pow R ℕ] [IsReduced R] (h : IsNilpotent x) : x = 0

@[simp]

theorem isNilpotent_iff_eq_zero {R : Type u_3} {x : R} [MonoidWithZero R] [IsReduced R] : IsNilpotent x ↔ x = 0

theorem exists_isNilpotent_of_not_isReduced {R : Type u_5} [Zero R] [Pow R ℕ] (h : ¬IsReduced R) : ∃ (x : R), x ≠ 0 ∧ IsNilpotent x

@[simp]

theorem zero_pow {M₀ : Type u_1} [MonoidWithZero M₀] {n : ℕ} : n ≠ 0 → 0 ^ n = 0

theorem zero_pow_eq {M₀ : Type u_1} [MonoidWithZero M₀] (n : ℕ) : 0 ^ n = if n = 0 then 1 else 0

theorem zero_pow_eq_one₀ {M₀ : Type u_1} [MonoidWithZero M₀] {n : ℕ} [Nontrivial M₀] : 0 ^ n = 1 ↔ n = 0

theorem pow_eq_zero_of_le {M₀ : Type u_1} [MonoidWithZero M₀] {a : M₀} {m n : ℕ} : m ≤ n → a ^ m = 0 → a ^ n = 0

theorem ne_zero_pow {M₀ : Type u_1} [MonoidWithZero M₀] {a : M₀} {n : ℕ} (hn : n ≠ 0) (ha : a ^ n ≠ 0) : a ≠ 0

@[simp]

theorem zero_pow_eq_zero {M₀ : Type u_1} [MonoidWithZero M₀] {n : ℕ} [Nontrivial M₀] : 0 ^ n = 0 ↔ n ≠ 0

theorem pow_mul_eq_zero_of_le {M₀ : Type u_1} [MonoidWithZero M₀] {a b : M₀} {m n : ℕ} (hmn : m ≤ n) (h : a ^ m * b = 0) : a ^ n * b = 0

@[instance 900]

instance isReduced_of_noZeroDivisors {M₀ : Type u_1} [MonoidWithZero M₀] [NoZeroDivisors M₀] : IsReduced M₀

@[deprecated eq_zero_of_pow_eq_zero (since := "2025-10-14")]

theorem pow_eq_zero {R : Type u_3} {x : R} [Zero R] [Pow R ℕ] [IsReduced R] {n : ℕ} (h : x ^ n = 0) : x = 0

Alias of eq_zero_of_pow_eq_zero.

@[simp]

theorem pow_eq_zero_iff {M₀ : Type u_1} [MonoidWithZero M₀] {a : M₀} {n : ℕ} [IsReduced M₀] (hn : n ≠ 0) : a ^ n = 0 ↔ a = 0

theorem pow_ne_zero_iff {M₀ : Type u_1} [MonoidWithZero M₀] {a : M₀} {n : ℕ} [IsReduced M₀] (hn : n ≠ 0) : a ^ n ≠ 0 ↔ a ≠ 0

theorem pow_ne_zero {M₀ : Type u_1} [MonoidWithZero M₀] {a : M₀} [IsReduced M₀] (n : ℕ) (h : a ≠ 0) : a ^ n ≠ 0

instance NeZero.pow {M₀ : Type u_1} [MonoidWithZero M₀] {a : M₀} {n : ℕ} [IsReduced M₀] [NeZero a] : NeZero (a ^ n)

theorem sq_eq_zero_iff {M₀ : Type u_1} [MonoidWithZero M₀] {a : M₀} [IsReduced M₀] : a ^ 2 = 0 ↔ a = 0

@[simp]

theorem pow_eq_zero_iff' {M₀ : Type u_1} [MonoidWithZero M₀] {a : M₀} {n : ℕ} [IsReduced M₀] [Nontrivial M₀] : a ^ n = 0 ↔ a = 0 ∧ n ≠ 0

A variant of pow_eq_zero_iff assuming M₀ is not trivial.

@[deprecated eq_zero_of_pow_eq_zero (since := "2026-01-08")]

theorem IsReduced.pow_eq_zero {R : Type u_3} {x : R} [Zero R] [Pow R ℕ] [IsReduced R] {n : ℕ} (h : x ^ n = 0) : x = 0

Alias of eq_zero_of_pow_eq_zero.

@[deprecated pow_eq_zero_iff (since := "2026-01-08")]

theorem IsReduced.pow_eq_zero_iff {M₀ : Type u_1} [MonoidWithZero M₀] {a : M₀} {n : ℕ} [IsReduced M₀] (hn : n ≠ 0) : a ^ n = 0 ↔ a = 0

Alias of pow_eq_zero_iff.

@[deprecated pow_ne_zero_iff (since := "2026-01-08")]

theorem IsReduced.pow_ne_zero_iff {M₀ : Type u_1} [MonoidWithZero M₀] {a : M₀} {n : ℕ} [IsReduced M₀] (hn : n ≠ 0) : a ^ n ≠ 0 ↔ a ≠ 0

Alias of pow_ne_zero_iff.

@[deprecated pow_ne_zero (since := "2026-01-08")]

theorem IsReduced.pow_ne_zero {M₀ : Type u_1} [MonoidWithZero M₀] {a : M₀} [IsReduced M₀] (n : ℕ) (h : a ≠ 0) : a ^ n ≠ 0

Alias of pow_ne_zero.

@[deprecated pow_eq_zero_iff' (since := "2026-01-08")]

theorem IsReduced.pow_eq_zero_iff' {M₀ : Type u_1} [MonoidWithZero M₀] {a : M₀} {n : ℕ} [IsReduced M₀] [Nontrivial M₀] : a ^ n = 0 ↔ a = 0 ∧ n ≠ 0

Alias of pow_eq_zero_iff'.

---

A variant of pow_eq_zero_iff assuming M₀ is not trivial.

theorem exists_right_inv_of_exists_left_inv {α : Type u_3} [MonoidWithZero α] (h : ∀ (a : α), a ≠ 0 → ∃ (b : α), b * a = 1) {a : α} (ha : a ≠ 0) : ∃ (b : α), a * b = 1

@[instance 10]

instance CancelMonoidWithZero.to_noZeroDivisors {M₀ : Type u_1} [CancelMonoidWithZero M₀] : NoZeroDivisors M₀

@[simp]

theorem mul_eq_mul_right_iff {M₀ : Type u_1} [CancelMonoidWithZero M₀] {a b c : M₀} : a * c = b * c ↔ a = b ∨ c = 0

@[simp]

theorem mul_eq_mul_left_iff {M₀ : Type u_1} [CancelMonoidWithZero M₀] {a b c : M₀} : a * b = a * c ↔ b = c ∨ a = 0

theorem mul_right_eq_self₀ {M₀ : Type u_1} [CancelMonoidWithZero M₀] {a b : M₀} : a * b = a ↔ b = 1 ∨ a = 0

theorem mul_left_eq_self₀ {M₀ : Type u_1} [CancelMonoidWithZero M₀] {a b : M₀} : a * b = b ↔ a = 1 ∨ b = 0

@[simp]

theorem mul_eq_left₀ {M₀ : Type u_1} [CancelMonoidWithZero M₀] {a b : M₀} (ha : a ≠ 0) : a * b = a ↔ b = 1

@[simp]

theorem mul_eq_right₀ {M₀ : Type u_1} [CancelMonoidWithZero M₀] {a b : M₀} (hb : b ≠ 0) : a * b = b ↔ a = 1

@[simp]

theorem left_eq_mul₀ {M₀ : Type u_1} [CancelMonoidWithZero M₀] {a b : M₀} (ha : a ≠ 0) : a = a * b ↔ b = 1

@[simp]

theorem right_eq_mul₀ {M₀ : Type u_1} [CancelMonoidWithZero M₀] {a b : M₀} (hb : b ≠ 0) : b = a * b ↔ a = 1

theorem eq_zero_of_mul_eq_self_right {M₀ : Type u_1} [CancelMonoidWithZero M₀] {a b : M₀} (h₁ : b ≠ 1) (h₂ : a * b = a) : a = 0

An element of a CancelMonoidWithZero fixed by right multiplication by an element other than one must be zero.

theorem eq_zero_of_mul_eq_self_left {M₀ : Type u_1} [CancelMonoidWithZero M₀] {a b : M₀} (h₁ : b ≠ 1) (h₂ : b * a = a) : a = 0

An element of a CancelMonoidWithZero fixed by left multiplication by an element other than one must be zero.

theorem GroupWithZero.mul_right_injective {G₀ : Type u_2} [GroupWithZero G₀] {x : G₀} (h : x ≠ 0) : Function.Injective fun (y : G₀) => x * y

theorem GroupWithZero.mul_left_injective {G₀ : Type u_2} [GroupWithZero G₀] {x : G₀} (h : x ≠ 0) : Function.Injective fun (y : G₀) => y * x

@[simp]

theorem inv_mul_cancel_right₀ {G₀ : Type u_2} [GroupWithZero G₀] {b : G₀} (h : b ≠ 0) (a : G₀) : a * b⁻¹ * b = a

@[simp]

theorem inv_mul_cancel_left₀ {G₀ : Type u_2} [GroupWithZero G₀] {a : G₀} (h : a ≠ 0) (b : G₀) : a⁻¹ * (a * b) = b

@[instance 100]

instance GroupWithZero.toDivisionMonoid {G₀ : Type u_2} [GroupWithZero G₀] : DivisionMonoid G₀

Equations

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

@[instance 10]

instance GroupWithZero.toCancelMonoidWithZero {G₀ : Type u_2} [GroupWithZero G₀] : CancelMonoidWithZero G₀

Equations

• GroupWithZero.toCancelMonoidWithZero = { toMonoidWithZero := inst✝.toMonoidWithZero, toIsCancelMulZero := ⋯ }

@[simp]

theorem zero_div {G₀ : Type u_2} [GroupWithZero G₀] (a : G₀) : 0 / a = 0

@[simp]

theorem div_zero {G₀ : Type u_2} [GroupWithZero G₀] (a : G₀) : a / 0 = 0

@[simp]

theorem mul_self_mul_inv {G₀ : Type u_2} [GroupWithZero G₀] (a : G₀) : a * a * a⁻¹ = a

Multiplying a by itself and then by its inverse results in a (whether or not a is zero).

@[simp]

theorem mul_inv_mul_cancel {G₀ : Type u_2} [GroupWithZero G₀] (a : G₀) : a * a⁻¹ * a = a

Multiplying a by its inverse and then by itself results in a (whether or not a is zero).

@[simp]

theorem inv_mul_mul_self {G₀ : Type u_2} [GroupWithZero G₀] (a : G₀) : a⁻¹ * a * a = a

Multiplying a⁻¹ by a twice results in a (whether or not a is zero).

@[simp]

theorem mul_self_div_self {G₀ : Type u_2} [GroupWithZero G₀] (a : G₀) : a * a / a = a

Multiplying a by itself and then dividing by itself results in a, whether or not a is zero.

@[simp]

theorem div_self_mul_self {G₀ : Type u_2} [GroupWithZero G₀] (a : G₀) : a / a * a = a

Dividing a by itself and then multiplying by itself results in a, whether or not a is zero.

@[simp]

theorem div_self_mul_self' {G₀ : Type u_2} [GroupWithZero G₀] (a : G₀) : a / (a * a) = a⁻¹

theorem one_div_ne_zero {G₀ : Type u_2} [GroupWithZero G₀] {a : G₀} (h : a ≠ 0) : 1 / a ≠ 0

@[simp]

theorem inv_eq_zero {G₀ : Type u_2} [GroupWithZero G₀] {a : G₀} : a⁻¹ = 0 ↔ a = 0

@[simp]

theorem zero_eq_inv {G₀ : Type u_2} [GroupWithZero G₀] {a : G₀} : 0 = a⁻¹ ↔ 0 = a

@[simp]

theorem div_div_self {G₀ : Type u_2} [GroupWithZero G₀] (a : G₀) : a / (a / a) = a

Dividing a by the result of dividing a by itself results in a (whether or not a is zero).

theorem ne_zero_of_one_div_ne_zero {G₀ : Type u_2} [GroupWithZero G₀] {a : G₀} (h : 1 / a ≠ 0) : a ≠ 0

theorem eq_zero_of_one_div_eq_zero {G₀ : Type u_2} [GroupWithZero G₀] {a : G₀} (h : 1 / a = 0) : a = 0

theorem mul_left_surjective₀ {G₀ : Type u_2} [GroupWithZero G₀] {a : G₀} (h : a ≠ 0) : Function.Surjective fun (g : G₀) => a * g

theorem mul_right_surjective₀ {G₀ : Type u_2} [GroupWithZero G₀] {a : G₀} (h : a ≠ 0) : Function.Surjective fun (g : G₀) => g * a

theorem zero_zpow {G₀ : Type u_2} [GroupWithZero G₀] (n : ℤ) : n ≠ 0 → 0 ^ n = 0

theorem zero_zpow_eq {G₀ : Type u_2} [GroupWithZero G₀] (n : ℤ) : 0 ^ n = if n = 0 then 1 else 0

theorem zero_zpow_eq_one₀ {G₀ : Type u_2} [GroupWithZero G₀] {n : ℤ} : 0 ^ n = 1 ↔ n = 0

theorem zpow_add_one₀ {G₀ : Type u_2} [GroupWithZero G₀] {a : G₀} (ha : a ≠ 0) (n : ℤ) : a ^ (n + 1) = a ^ n * a

theorem zpow_sub_one₀ {G₀ : Type u_2} [GroupWithZero G₀] {a : G₀} (ha : a ≠ 0) (n : ℤ) : a ^ (n - 1) = a ^ n * a⁻¹

theorem zpow_add₀ {G₀ : Type u_2} [GroupWithZero G₀] {a : G₀} (ha : a ≠ 0) (m n : ℤ) : a ^ (m + n) = a ^ m * a ^ n

theorem zpow_add' {G₀ : Type u_2} [GroupWithZero G₀] {a : G₀} {m n : ℤ} (h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0) : a ^ (m + n) = a ^ m * a ^ n

theorem zpow_one_add₀ {G₀ : Type u_2} [GroupWithZero G₀] {a : G₀} (h : a ≠ 0) (i : ℤ) : a ^ (1 + i) = a * a ^ i

theorem div_mul_eq_mul_div₀ {G₀ : Type u_2} [CommGroupWithZero G₀] (a b c : G₀) : a / c * b = a * b / c

theorem div_sq_cancel {G₀ : Type u_2} [CommGroupWithZero G₀] (a b : G₀) : a ^ 2 * b / a = a * b