doc-next-gen

Mathlib.Algebra.GroupWithZero.Basic

Module docstring

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

"}

left_ne_zero_of_mul theorem
: a * b ≠ 0 → a ≠ 0
Full source 
theorem left_ne_zero_of_mul : a * b ≠ 0 → a ≠ 0 :=
  mt fun h => mul_eq_zero_of_left h b
Nonzero Product Implies Nonzero Left Factor in Group with Zero
Informal description
For any elements $a$ and $b$ in a group with zero, if the product $a \cdot b$ is nonzero, then $a$ is nonzero.
right_ne_zero_of_mul theorem
: a * b ≠ 0 → b ≠ 0
Full source 
theorem right_ne_zero_of_mul : a * b ≠ 0 → b ≠ 0 :=
  mt (mul_eq_zero_of_right a)
Nonzero Product Implies Nonzero Right Factor
Informal description
For any elements $a$ and $b$ in a monoid with zero, if the product $a \cdot b$ is nonzero, then $b$ is nonzero.
mul_eq_zero_of_ne_zero_imp_eq_zero theorem
{a b : M₀} (h : a ≠ 0 → b = 0) : a * b = 0
Full source 
theorem mul_eq_zero_of_ne_zero_imp_eq_zero {a b : M₀} (h : a ≠ 0 → b = 0) : a * b = 0 := by
  have : Decidable (a = 0) := Classical.propDecidable (a = 0)
  exact if ha : a = 0 then by rw [ha, zero_mul] else by rw [h ha, mul_zero]
Product is zero when non-zero implies zero
Informal description
For any elements $a$ and $b$ in a monoid with zero $M_0$, if $a \neq 0$ implies $b = 0$, then the product $a \cdot b$ is equal to $0$.
zero_mul_eq_const theorem
: ((0 : M₀) * ·) = Function.const _ 0
Full source 
/-- To match `one_mul_eq_id`. -/
theorem zero_mul_eq_const : ((0 : M₀) * ·) = Function.const _ 0 :=
  funext zero_mul
Left Multiplication by Zero Yields Zero in Monoid with Zero
Informal description
For any element $x$ in a monoid with zero $M₀$, multiplying zero on the left by $x$ yields zero, i.e., $0 \cdot x = 0$. This can be expressed as the function $x \mapsto 0 \cdot x$ being equal to the constant zero function.
mul_zero_eq_const theorem
: (· * (0 : M₀)) = Function.const _ 0
Full source 
/-- To match `mul_one_eq_id`. -/
theorem mul_zero_eq_const : (· * (0 : M₀)) = Function.const _ 0 :=
  funext mul_zero
Right Multiplication by Zero Yields Zero in Monoids with Zero
Informal description
For any element $x$ in a monoid with zero $M₀$, the multiplication of $x$ by zero equals zero, i.e., $x * 0 = 0$. This is expressed as the function $x \mapsto x * 0$ being equal to the constant zero function.
mul_ne_zero theorem
(ha : a ≠ 0) (hb : b ≠ 0) : a * b ≠ 0
Full source 
@[field_simps]
theorem mul_ne_zero (ha : a ≠ 0) (hb : b ≠ 0) : a * b ≠ 0 :=
  mt eq_zero_or_eq_zero_of_mul_eq_zero <| not_or.mpr ⟨ha, hb⟩
Nonzero Elements Multiply to Nonzero in Group with Zero
Informal description
For any elements $a$ and $b$ in a group with zero, if $a \neq 0$ and $b \neq 0$, then their product $a * b \neq 0$.
NeZero.mul instance
[Zero M₀] [Mul M₀] [NoZeroDivisors M₀] {x y : M₀} [NeZero x] [NeZero y] : NeZero (x * y)
Full source 
instance mul [Zero M₀] [Mul M₀] [NoZeroDivisors M₀] {x y : M₀} [NeZero x] [NeZero y] :
    NeZero (x * y) :=
  ⟨mul_ne_zero out out⟩
Product of Nonzero Elements is Nonzero in No-Zero-Divisors Semigroups
Informal description
For any type $M₀$ with zero and multiplication operations and satisfying the no-zero-divisors property, if $x$ and $y$ are nonzero elements of $M₀$, then their product $x * y$ is also nonzero.
uniqueOfZeroEqOne definition
(h : (0 : M₀) = 1) : Unique M₀
Full source 
/-- 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. -/
def uniqueOfZeroEqOne (h : (0 : M₀) = 1) : Unique M₀ where
  default := 0
  uniq := eq_zero_of_zero_eq_one h
Uniqueness of zero in a monoid with zero when zero equals one
Informal description
In a monoid with zero, if the zero element equals the one element (i.e., $0 = 1$), then the monoid has exactly one element, which is zero. This element is uniquely determined as the default element of the monoid.
subsingleton_iff_zero_eq_one theorem
: (0 : M₀) = 1 ↔ Subsingleton M₀
Full source 
/-- In a monoid with zero, zero equals one if and only if all elements of that semiring
are equal. -/
theorem subsingleton_iff_zero_eq_one : (0 : M₀) = 1 ↔ Subsingleton M₀ :=
  ⟨fun h => haveI := uniqueOfZeroEqOne h; inferInstance, fun h => @Subsingleton.elim _ h _ _⟩
Characterization of Trivial Monoid with Zero: $0 = 1$ iff $M_0$ is a Subsingleton
Informal description
In a monoid with zero $M_0$, the zero element equals the multiplicative identity (i.e., $0 = 1$) if and only if $M_0$ is a subsingleton (i.e., has at most one element).
zero_ne_one_or_forall_eq_0 theorem
: (0 : M₀) ≠ 1 ∨ ∀ a : M₀, a = 0
Full source 
/-- In a monoid with zero, either zero and one are nonequal, or zero is the only element. -/
theorem zero_ne_one_or_forall_eq_0 : (0 : M₀) ≠ 1(0 : M₀) ≠ 1 ∨ ∀ a : M₀, a = 0 :=
  not_or_of_imp eq_zero_of_zero_eq_one
Distinctness of Zero and One or Triviality in Monoid with Zero
Informal description
In a monoid with zero $M_0$, either the zero element and the multiplicative identity are distinct ($0 \neq 1$), or every element of $M_0$ is equal to zero ($\forall a \in M_0, a = 0$).
left_ne_zero_of_mul_eq_one theorem
(h : a * b = 1) : a ≠ 0
Full source 
theorem left_ne_zero_of_mul_eq_one (h : a * b = 1) : a ≠ 0 :=
  left_ne_zero_of_mul <| ne_zero_of_eq_one h
Nonzero Left Factor in Group with Zero from Product Identity
Informal description
For any elements $a$ and $b$ in a group with zero, if $a \cdot b = 1$, then $a \neq 0$.
right_ne_zero_of_mul_eq_one theorem
(h : a * b = 1) : b ≠ 0
Full source 
theorem right_ne_zero_of_mul_eq_one (h : a * b = 1) : b ≠ 0 :=
  right_ne_zero_of_mul <| ne_zero_of_eq_one h
Nonzero Right Factor in Group with Zero from Product Identity
Informal description
For any elements $a$ and $b$ in a group with zero, if $a \cdot b = 1$, then $b \neq 0$.
zero_pow theorem
: ∀ {n : ℕ}, n ≠ 0 → (0 : M₀) ^ n = 0
Full source 
@[simp] lemma zero_pow : ∀ {n : ℕ}, n ≠ 0 → (0 : M₀) ^ n = 0
  | n + 1, _ => by rw [pow_succ, mul_zero]
Zero to a Positive Power is Zero in a Group with Zero
Informal description
For any natural number $n \neq 0$ and any element $0$ in a group with zero $M_0$, the $n$-th power of $0$ equals $0$, i.e., $0^n = 0$.
zero_pow_eq theorem
(n : ℕ) : (0 : M₀) ^ n = if n = 0 then 1 else 0
Full source 
lemma zero_pow_eq (n : ℕ) : (0 : M₀) ^ n = if n = 0 then 1 else 0 := by
  split_ifs with h
  · rw [h, pow_zero]
  · rw [zero_pow h]
Power of Zero: $0^n = \begin{cases} 1 & n=0 \\ 0 & n \neq 0 \end{cases}$
Informal description
For any natural number $n$ and the zero element $0$ in a group with zero $M_0$, the $n$-th power of $0$ equals $1$ if $n = 0$ and equals $0$ otherwise, i.e., $$ 0^n = \begin{cases} 1 & \text{if } n = 0, \\ 0 & \text{otherwise.} \end{cases} $$
zero_pow_eq_one₀ theorem
[Nontrivial M₀] : (0 : M₀) ^ n = 1 ↔ n = 0
Full source 
lemma zero_pow_eq_one₀ [Nontrivial M₀] : (0 : M₀) ^ n = 1 ↔ n = 0 := by
  rw [zero_pow_eq, one_ne_zero.ite_eq_left_iff]
Zero to a Power Equals One if and only if Exponent is Zero in Nontrivial Group with Zero
Informal description
In a nontrivial group with zero $M_0$, the zero element raised to the power $n$ equals the multiplicative identity $1$ if and only if $n = 0$. That is, $$ 0^n = 1 \leftrightarrow n = 0. $$
pow_eq_zero_of_le theorem
: ∀ {m n}, m ≤ n → a ^ m = 0 → a ^ n = 0
Full source 
lemma pow_eq_zero_of_le : ∀ {m n}, m ≤ n → a ^ m = 0 → a ^ n = 0
  | _, _, Nat.le.refl, ha => ha
  | _, _, Nat.le.step hmn, ha => by rw [pow_succ, pow_eq_zero_of_le hmn ha, zero_mul]
Power of Zero Propagation: $a^m = 0 \implies a^n = 0$ for $m \leq n$
Informal description
For any elements $a$ in a monoid with zero $M₀$ and natural numbers $m \leq n$, if $a^m = 0$ then $a^n = 0$.
ne_zero_pow theorem
(hn : n ≠ 0) (ha : a ^ n ≠ 0) : a ≠ 0
Full source 
lemma ne_zero_pow (hn : n ≠ 0) (ha : a ^ n ≠ 0) : a ≠ 0 := by rintro rfl; exact ha <| zero_pow hn
Nonzero Power Implies Nonzero Base: $a^n \neq 0 \implies a \neq 0$ for $n \neq 0$
Informal description
For any element $a$ in a monoid with zero and any natural number $n \neq 0$, if $a^n \neq 0$ then $a \neq 0$.
zero_pow_eq_zero theorem
[Nontrivial M₀] : (0 : M₀) ^ n = 0 ↔ n ≠ 0
Full source 
@[simp]
lemma zero_pow_eq_zero [Nontrivial M₀] : (0 : M₀) ^ n = 0 ↔ n ≠ 0 :=
  ⟨by rintro h rfl; simp at h, zero_pow⟩
Zero Power Identity in Nontrivial Groups with Zero: $0^n = 0 \leftrightarrow n \neq 0$
Informal description
Let $M_0$ be a nontrivial group with zero. For any natural number $n$, the $n$-th power of zero equals zero if and only if $n$ is nonzero, i.e., $0^n = 0 \leftrightarrow n \neq 0$.
pow_mul_eq_zero_of_le theorem
{a b : M₀} {m n : ℕ} (hmn : m ≤ n) (h : a ^ m * b = 0) : a ^ n * b = 0
Full source 
lemma pow_mul_eq_zero_of_le {a b : M₀} {m n : ℕ} (hmn : m ≤ n)
    (h : a ^ m * b = 0) : a ^ n * b = 0 := by
  rw [show n = n - m + m by omega, pow_add, mul_assoc, h]
  simp
Vanishing of Higher Powers in Monoids with Zero: $a^m b = 0 \implies a^n b = 0$ for $m \leq n$
Informal description
Let $M₀$ be a monoid with zero, and let $a, b \in M₀$. For any natural numbers $m, n$ with $m \leq n$, if $a^m \cdot b = 0$, then $a^n \cdot b = 0$.
pow_eq_zero theorem
: ∀ {n}, a ^ n = 0 → a = 0
Full source 
lemma pow_eq_zero : ∀ {n}, a ^ n = 0 → a = 0
  | 0, ha => by simpa using congr_arg (a * ·) ha
  | n + 1, ha => by rw [pow_succ, mul_eq_zero] at ha; exact ha.elim pow_eq_zero id
Vanishing of Powers Implies Vanishing of Base in Monoids with Zero
Informal description
For any element $a$ in a monoid with zero $M₀$ and any natural number $n$, if $a^n = 0$ then $a = 0$.
pow_eq_zero_iff theorem
(hn : n ≠ 0) : a ^ n = 0 ↔ a = 0
Full source 
@[simp] lemma pow_eq_zero_iff (hn : n ≠ 0) : a ^ n = 0 ↔ a = 0 :=
  ⟨pow_eq_zero, by rintro rfl; exact zero_pow hn⟩
Equivalence of Vanishing Power and Vanishing Base in Monoids with Zero
Informal description
For any element $a$ in a monoid with zero $M₀$ and any nonzero natural number $n$, the $n$-th power of $a$ equals zero if and only if $a$ itself equals zero, i.e., $a^n = 0 \leftrightarrow a = 0$.
pow_ne_zero_iff theorem
(hn : n ≠ 0) : a ^ n ≠ 0 ↔ a ≠ 0
Full source 
lemma pow_ne_zero_iff (hn : n ≠ 0) : a ^ n ≠ 0a ^ n ≠ 0 ↔ a ≠ 0 := (pow_eq_zero_iff hn).not
Nonzero Power Equivalence in Monoids with Zero: $a^n \neq 0 \leftrightarrow a \neq 0$ for $n \neq 0$
Informal description
For any element $a$ in a monoid with zero and any nonzero natural number $n$, the $n$-th power of $a$ is nonzero if and only if $a$ itself is nonzero, i.e., $a^n \neq 0 \leftrightarrow a \neq 0$.
pow_ne_zero theorem
(n : ℕ) (h : a ≠ 0) : a ^ n ≠ 0
Full source 
@[field_simps]
lemma pow_ne_zero (n : ℕ) (h : a ≠ 0) : a ^ n ≠ 0 := mt pow_eq_zero h
Nonzero Elements Have Nonzero Powers in Monoids with Zero
Informal description
For any element $a$ in a monoid with zero and any natural number $n$, if $a \neq 0$, then $a^n \neq 0$.
NeZero.pow instance
[NeZero a] : NeZero (a ^ n)
Full source 
instance NeZero.pow [NeZero a] : NeZero (a ^ n) := ⟨pow_ne_zero n NeZero.out⟩
Nonzero Elements Have Nonzero Powers in Monoids with Zero
Informal description
For any element $a$ in a monoid with zero and any natural number $n$, if $a$ is nonzero, then $a^n$ is also nonzero.
sq_eq_zero_iff theorem
: a ^ 2 = 0 ↔ a = 0
Full source 
lemma sq_eq_zero_iff : a ^ 2 = 0 ↔ a = 0 := pow_eq_zero_iff two_ne_zero
Square Equals Zero Criterion: $a^2 = 0 \leftrightarrow a = 0$
Informal description
For any element $a$ in a monoid with zero, the square of $a$ equals zero if and only if $a$ itself equals zero, i.e., $a^2 = 0 \leftrightarrow a = 0$.
pow_eq_zero_iff' theorem
[Nontrivial M₀] : a ^ n = 0 ↔ a = 0 ∧ n ≠ 0
Full source 
@[simp] lemma pow_eq_zero_iff' [Nontrivial M₀] : a ^ n = 0 ↔ a = 0 ∧ n ≠ 0 := by
  obtain rfl | hn := eq_or_ne n 0 <;> simp [*]
Power Equals Zero Criterion in Nontrivial Monoids with Zero: $a^n = 0 \leftrightarrow (a = 0 \land n \neq 0)$
Informal description
In a nontrivial monoid with zero $M_0$, for any element $a \in M_0$ and natural number $n$, the power $a^n$ equals zero if and only if $a = 0$ and $n \neq 0$.
exists_right_inv_of_exists_left_inv theorem
{α} [MonoidWithZero α] (h : ∀ a : α, a ≠ 0 → ∃ b : α, b * a = 1) {a : α} (ha : a ≠ 0) : ∃ b : α, a * b = 1
Full source 
theorem exists_right_inv_of_exists_left_inv {α} [MonoidWithZero α]
    (h : ∀ a : α, a ≠ 0 → ∃ b : α, b * a = 1) {a : α} (ha : a ≠ 0) : ∃ b : α, a * b = 1 := by
  obtain _ | _ := subsingleton_or_nontrivial α
  · exact ⟨a, Subsingleton.elim _ _⟩
  obtain ⟨b, hb⟩ := h a ha
  obtain ⟨c, hc⟩ := h b (left_ne_zero_of_mul <| hb.trans_ne one_ne_zero)
  refine ⟨b, ?_⟩
  conv_lhs => rw [← one_mul (a * b), ← hc, mul_assoc, ← mul_assoc b, hb, one_mul, hc]
Existence of Right Inverse from Left Inverse in Monoid with Zero
Informal description
Let $\alpha$ be a monoid with zero. Suppose that for every nonzero element $a \in \alpha$, there exists an element $b \in \alpha$ such that $b \cdot a = 1$. Then for any nonzero element $a \in \alpha$, there exists an element $b \in \alpha$ such that $a \cdot b = 1$.
CancelMonoidWithZero.to_noZeroDivisors instance
: NoZeroDivisors M₀
Full source 
instance (priority := 10) CancelMonoidWithZero.to_noZeroDivisors : NoZeroDivisors M₀ :=
  ⟨fun ab0 => or_iff_not_imp_left.mpr fun ha => mul_left_cancel₀ ha <|
    ab0.trans (mul_zero _).symm⟩
Cancel Monoids with Zero Have No Zero Divisors
Informal description
Every cancel monoid with zero has no zero divisors. That is, for any elements $a$ and $b$ in the monoid, if $a \cdot b = 0$, then either $a = 0$ or $b = 0$.
mul_eq_mul_right_iff theorem
: a * c = b * c ↔ a = b ∨ c = 0
Full source 
@[simp]
theorem mul_eq_mul_right_iff : a * c = b * c ↔ a = b ∨ c = 0 := by
  by_cases hc : c = 0 <;> [simp only [hc, mul_zero, or_true]; simp [mul_left_inj', hc]]
Right Cancellation in Monoid with Zero: $a \cdot c = b \cdot c \leftrightarrow a = b \lor c = 0$
Informal description
For elements $a$, $b$, and $c$ in a monoid with zero, the equality $a \cdot c = b \cdot c$ holds if and only if either $a = b$ or $c = 0$.
mul_eq_left₀ theorem
(ha : a ≠ 0) : a * b = a ↔ b = 1
Full source 
@[simp]
theorem mul_eq_left₀ (ha : a ≠ 0) : a * b = a ↔ b = 1 := by
  rw [Iff.comm, ← mul_right_inj' ha, mul_one]
Left multiplication identity in a group with zero: $a \cdot b = a \leftrightarrow b = 1$ for $a \neq 0$
Informal description
For any nonzero element $a$ in a group with zero, the equation $a \cdot b = a$ holds if and only if $b = 1$.
mul_eq_right₀ theorem
(hb : b ≠ 0) : a * b = b ↔ a = 1
Full source 
@[simp]
theorem mul_eq_right₀ (hb : b ≠ 0) : a * b = b ↔ a = 1 := by
  rw [Iff.comm, ← mul_left_inj' hb, one_mul]
Right multiplication identity in a group with zero: $a \cdot b = b \leftrightarrow a = 1$ for $b \neq 0$
Informal description
For any elements $a$ and $b$ in a group with zero, if $b \neq 0$, then $a \cdot b = b$ if and only if $a = 1$.
left_eq_mul₀ theorem
(ha : a ≠ 0) : a = a * b ↔ b = 1
Full source 
@[simp]
theorem left_eq_mul₀ (ha : a ≠ 0) : a = a * b ↔ b = 1 := by rw [eq_comm, mul_eq_left₀ ha]
Left Equality in Group with Zero: $a = a \cdot b \leftrightarrow b = 1$ for $a \neq 0$
Informal description
For any nonzero element $a$ in a group with zero, the equality $a = a \cdot b$ holds if and only if $b = 1$.
right_eq_mul₀ theorem
(hb : b ≠ 0) : b = a * b ↔ a = 1
Full source 
@[simp]
theorem right_eq_mul₀ (hb : b ≠ 0) : b = a * b ↔ a = 1 := by rw [eq_comm, mul_eq_right₀ hb]
Right equality with multiplication in a group with zero: $b = a \cdot b \leftrightarrow a = 1$ for $b \neq 0$
Informal description
For any elements $a$ and $b$ in a group with zero, if $b \neq 0$, then $b = a \cdot b$ if and only if $a = 1$.
GroupWithZero.mul_right_injective theorem
(h : x ≠ 0) : Function.Injective fun y => x * y
Full source 
theorem GroupWithZero.mul_right_injective (h : x ≠ 0) :
    Function.Injective fun y => x * y := fun y y' w => by
  simpa only [← mul_assoc, inv_mul_cancel₀ h, one_mul] using congr_arg (fun y => x⁻¹ * y) w
Right multiplication by a nonzero element is injective in a group with zero
Informal description
For any nonzero element $x$ in a group with zero $G₀$, the function $y \mapsto x \cdot y$ is injective.
GroupWithZero.mul_left_injective theorem
(h : x ≠ 0) : Function.Injective fun y => y * x
Full source 
theorem GroupWithZero.mul_left_injective (h : x ≠ 0) :
    Function.Injective fun y => y * x := fun y y' w => by
  simpa only [mul_assoc, mul_inv_cancel₀ h, mul_one] using congr_arg (fun y => y * x⁻¹) w
Left multiplication by a nonzero element is injective in a group with zero
Informal description
For any nonzero element $x$ in a group with zero $G₀$, the function $y \mapsto y \cdot x$ is injective.
inv_mul_cancel_right₀ theorem
(h : b ≠ 0) (a : G₀) : a * b⁻¹ * b = a
Full source 
@[simp]
theorem inv_mul_cancel_right₀ (h : b ≠ 0) (a : G₀) : a * b⁻¹ * b = a :=
  calc
    a * b⁻¹ * b = a * (b⁻¹ * b) := mul_assoc _ _ _
    _ = a := by simp [h]
Right inverse cancellation in a group with zero: $(a b^{-1}) b = a$ for $b \neq 0$
Informal description
For any nonzero element $b$ in a group with zero $G₀$ and any element $a \in G₀$, the following identity holds: $(a \cdot b^{-1}) \cdot b = a$.
inv_mul_cancel_left₀ theorem
(h : a ≠ 0) (b : G₀) : a⁻¹ * (a * b) = b
Full source 
@[simp]
theorem inv_mul_cancel_left₀ (h : a ≠ 0) (b : G₀) : a⁻¹ * (a * b) = b :=
  calc
    a⁻¹ * (a * b) = a⁻¹ * a * b := (mul_assoc _ _ _).symm
    _ = b := by simp [h]
Left inverse cancellation in a group with zero: $a^{-1}(a b) = b$ for $a \neq 0$
Informal description
For any nonzero element $a$ in a group with zero $G_0$ and any element $b \in G_0$, the following identity holds: $a^{-1} \cdot (a \cdot b) = b$.
GroupWithZero.toDivisionMonoid instance
: DivisionMonoid G₀
Full source 
instance (priority := 100) GroupWithZero.toDivisionMonoid : DivisionMonoid G₀ :=
  { ‹GroupWithZero G₀› with
    inv := Inv.inv,
    inv_inv := fun a => by
      by_cases h : a = 0
      · simp [h]
      · exact left_inv_eq_right_inv (inv_mul_cancel₀ <| inv_ne_zero h) (inv_mul_cancel₀ h)
        ,
    mul_inv_rev := fun a b => by
      by_cases ha : a = 0
      · simp [ha]
      by_cases hb : b = 0
      · simp [hb]
      apply inv_eq_of_mul
      simp [mul_assoc, ha, hb],
    inv_eq_of_mul := fun _ _ => inv_eq_of_mul }
Groups with Zero are Division Monoids
Informal description
Every group with zero is a division monoid.
GroupWithZero.toCancelMonoidWithZero instance
: CancelMonoidWithZero G₀
Full source 
instance (priority := 10) GroupWithZero.toCancelMonoidWithZero : CancelMonoidWithZero G₀ :=
  { (‹_› : GroupWithZero G₀) with
    mul_left_cancel_of_ne_zero := @fun x y z hx h => by
      rw [← inv_mul_cancel_left₀ hx y, h, inv_mul_cancel_left₀ hx z],
    mul_right_cancel_of_ne_zero := @fun x y z hy h => by
      rw [← mul_inv_cancel_right₀ hy x, h, mul_inv_cancel_right₀ hy z] }
Groups with Zero are Cancel Monoids with Zero
Informal description
Every group with zero is a cancel monoid with zero.
zero_div theorem
(a : G₀) : 0 / a = 0
Full source 
@[simp]
theorem zero_div (a : G₀) : 0 / a = 0 := by rw [div_eq_mul_inv, zero_mul]
Division of Zero by Any Element in a Group with Zero
Informal description
For any element $a$ in a group with zero $G_0$, the division of zero by $a$ equals zero, i.e., $0 / a = 0$.
div_zero theorem
(a : G₀) : a / 0 = 0
Full source 
@[simp]
theorem div_zero (a : G₀) : a / 0 = 0 := by rw [div_eq_mul_inv, inv_zero, mul_zero]
Division by Zero Yields Zero in Groups with Zero
Informal description
For any element $a$ in a group with zero $G_0$, the division of $a$ by zero equals zero, i.e., $a / 0 = 0$.
mul_self_mul_inv theorem
(a : G₀) : a * a * a⁻¹ = a
Full source 
/-- Multiplying `a` by itself and then by its inverse results in `a`
(whether or not `a` is zero). -/
@[simp]
theorem mul_self_mul_inv (a : G₀) : a * a * a⁻¹ = a := by
  by_cases h : a = 0
  · rw [h, inv_zero, mul_zero]
  · rw [mul_assoc, mul_inv_cancel₀ h, mul_one]
Self-multiplication followed by inversion yields original element in group with zero
Informal description
For any element $a$ in a group with zero $G_0$, the product $a \cdot a \cdot a^{-1}$ equals $a$.
mul_inv_mul_cancel theorem
(a : G₀) : a * a⁻¹ * a = a
Full source 
/-- Multiplying `a` by its inverse and then by itself results in `a`
(whether or not `a` is zero). -/
@[simp]
theorem mul_inv_mul_cancel (a : G₀) : a * a⁻¹ * a = a := by
  by_cases h : a = 0
  · rw [h, inv_zero, mul_zero]
  · rw [mul_inv_cancel₀ h, one_mul]
Inverse-multiplication identity in a group with zero: $a \cdot a^{-1} \cdot a = a$
Informal description
For any element $a$ in a group with zero $G_0$, the product $a \cdot a^{-1} \cdot a$ equals $a$.
inv_mul_mul_self theorem
(a : G₀) : a⁻¹ * a * a = a
Full source 
/-- Multiplying `a⁻¹` by `a` twice results in `a` (whether or not `a`
is zero). -/
@[simp]
theorem inv_mul_mul_self (a : G₀) : a⁻¹ * a * a = a := by
  by_cases h : a = 0
  · rw [h, inv_zero, mul_zero]
  · rw [inv_mul_cancel₀ h, one_mul]
Inverse-multiplication identity in a group with zero: $a^{-1} \cdot a \cdot a = a$
Informal description
For any element $a$ in a group with zero $G_0$, the product $a^{-1} \cdot a \cdot a$ equals $a$.
mul_self_div_self theorem
(a : G₀) : a * a / a = a
Full source 
/-- Multiplying `a` by itself and then dividing by itself results in `a`, whether or not `a` is
zero. -/
@[simp]
theorem mul_self_div_self (a : G₀) : a * a / a = a := by rw [div_eq_mul_inv, mul_self_mul_inv a]
Self-multiplication and division identity: $(a \cdot a)/a = a$ in a group with zero
Informal description
For any element $a$ in a group with zero $G_0$, the operation $(a \cdot a) / a$ equals $a$.
div_self_mul_self theorem
(a : G₀) : a / a * a = a
Full source 
/-- Dividing `a` by itself and then multiplying by itself results in `a`, whether or not `a` is
zero. -/
@[simp]
theorem div_self_mul_self (a : G₀) : a / a * a = a := by rw [div_eq_mul_inv, mul_inv_mul_cancel a]
Self-division-multiplication identity in a group with zero: $(a/a) \cdot a = a$
Informal description
For any element $a$ in a group with zero $G_0$, the operation $(a / a) \cdot a$ equals $a$.
div_self_mul_self' theorem
(a : G₀) : a / (a * a) = a⁻¹
Full source 
@[simp]
theorem div_self_mul_self' (a : G₀) : a / (a * a) = a⁻¹ :=
  calc
    a / (a * a) = a⁻¹a⁻¹⁻¹ * a⁻¹ * a⁻¹ := by simp [mul_inv_rev]
    _ = a⁻¹ := inv_mul_mul_self _
Division Identity: $a/(a \cdot a) = a^{-1}$ in a Group with Zero
Informal description
For any element $a$ in a group with zero $G_0$, the division of $a$ by $a \cdot a$ equals the inverse of $a$, i.e., $a / (a \cdot a) = a^{-1}$.
one_div_ne_zero theorem
{a : G₀} (h : a ≠ 0) : 1 / a ≠ 0
Full source 
theorem one_div_ne_zero {a : G₀} (h : a ≠ 0) : 1 / a ≠ 0 := by
  simpa only [one_div] using inv_ne_zero h
Nonzero Reciprocal of Nonzero Element in Group with Zero
Informal description
For any nonzero element $a$ in a group with zero $G_0$, the reciprocal $1/a$ is nonzero.
inv_eq_zero theorem
{a : G₀} : a⁻¹ = 0 ↔ a = 0
Full source 
@[simp]
theorem inv_eq_zero {a : G₀} : a⁻¹a⁻¹ = 0 ↔ a = 0 := by rw [inv_eq_iff_eq_inv, inv_zero]
Inverse Equals Zero if and only if Element is Zero in Group with Zero
Informal description
For any element $a$ in a group with zero $G_0$, the inverse of $a$ equals zero if and only if $a$ equals zero, i.e., $a^{-1} = 0 \leftrightarrow a = 0$.
zero_eq_inv theorem
{a : G₀} : 0 = a⁻¹ ↔ 0 = a
Full source 
@[simp]
theorem zero_eq_inv {a : G₀} : 0 = a⁻¹ ↔ 0 = a :=
  eq_comm.trans <| inv_eq_zero.trans eq_comm
Zero Equals Inverse if and only if Zero Equals Element in Group with Zero
Informal description
For any element $a$ in a group with zero $G_0$, the equality $0 = a^{-1}$ holds if and only if $0 = a$.
div_div_self theorem
(a : G₀) : a / (a / a) = a
Full source 
/-- Dividing `a` by the result of dividing `a` by itself results in
`a` (whether or not `a` is zero). -/
@[simp]
theorem div_div_self (a : G₀) : a / (a / a) = a := by
  rw [div_div_eq_mul_div]
  exact mul_self_div_self a
Division Identity: $a/(a/a) = a$ in a Group with Zero
Informal description
For any element $a$ in a group with zero $G_0$, the operation $a / (a / a)$ equals $a$.
ne_zero_of_one_div_ne_zero theorem
{a : G₀} (h : 1 / a ≠ 0) : a ≠ 0
Full source 
theorem ne_zero_of_one_div_ne_zero {a : G₀} (h : 1 / a ≠ 0) : a ≠ 0 := fun ha : a = 0 => by
  rw [ha, div_zero] at h
  contradiction
Nonzero Reciprocal Implies Nonzero Element in Group with Zero
Informal description
For any element $a$ in a group with zero $G_0$, if the reciprocal of $a$ is nonzero (i.e., $1 / a \neq 0$), then $a$ itself is nonzero (i.e., $a \neq 0$).
zero_zpow theorem
: ∀ n : ℤ, n ≠ 0 → (0 : G₀) ^ n = 0
Full source 
lemma zero_zpow : ∀ n : ℤ, n ≠ 0 → (0 : G₀) ^ n = 0
  | (n : ℕ), h => by rw [zpow_natCast, zero_pow]; simpa [Int.natCast_eq_zero] using h
  | .negSucc n, _ => by simp
Zero to a Nonzero Integer Power is Zero in a Group with Zero
Informal description
For any integer $n \neq 0$ and any element $0$ in a group with zero $G_0$, the $n$-th power of $0$ equals $0$, i.e., $0^n = 0$.
zero_zpow_eq theorem
(n : ℤ) : (0 : G₀) ^ n = if n = 0 then 1 else 0
Full source 
lemma zero_zpow_eq (n : ℤ) : (0 : G₀) ^ n = if n = 0 then 1 else 0 := by
  split_ifs with h
  · rw [h, zpow_zero]
  · rw [zero_zpow _ h]
Zero Power Law in Groups with Zero: $0^n = \text{if } n = 0 \text{ then } 1 \text{ else } 0$
Informal description
For any integer $n$ and the zero element $0$ in a group with zero $G_0$, the $n$-th power of $0$ is equal to $1$ if $n = 0$ and $0$ otherwise, i.e., $$ 0^n = \begin{cases} 1 & \text{if } n = 0, \\ 0 & \text{otherwise.} \end{cases} $$
zero_zpow_eq_one₀ theorem
{n : ℤ} : (0 : G₀) ^ n = 1 ↔ n = 0
Full source 
lemma zero_zpow_eq_one₀ {n : ℤ} : (0 : G₀) ^ n = 1 ↔ n = 0 := by
  rw [zero_zpow_eq, one_ne_zero.ite_eq_left_iff]
Zero Power Equals One if and only if Exponent is Zero: $0^n = 1 \leftrightarrow n = 0$
Informal description
For any integer $n$ and the zero element $0$ in a group with zero $G_0$, the $n$-th power of $0$ equals $1$ if and only if $n = 0$, i.e., $$ 0^n = 1 \leftrightarrow n = 0. $$
zpow_add_one₀ theorem
(ha : a ≠ 0) : ∀ n : ℤ, a ^ (n + 1) = a ^ n * a
Full source 
lemma zpow_add_one₀ (ha : a ≠ 0) : ∀ n : ℤ, a ^ (n + 1) = a ^ n * a
  | (n : ℕ) => by simp only [← Int.natCast_succ, zpow_natCast, pow_succ]
  | -1 => by simp [ha]
  | .negSucc (n + 1) => by
    rw [Int.negSucc_eq, zpow_neg, Int.neg_add, Int.neg_add_cancel_right, zpow_neg,
      ← Int.natCast_succ, zpow_natCast, zpow_natCast, pow_succ' _ (n + 1), mul_inv_rev, mul_assoc,
      inv_mul_cancel₀ ha, mul_one]
Recursive power formula in groups with zero: $a^{n+1} = a^n \cdot a$
Informal description
For any nonzero element $a$ in a group with zero $G_0$ and any integer $n$, the $(n+1)$-th power of $a$ equals the $n$-th power of $a$ multiplied by $a$, i.e., $a^{n+1} = a^n \cdot a$.
zpow_sub_one₀ theorem
(ha : a ≠ 0) (n : ℤ) : a ^ (n - 1) = a ^ n * a⁻¹
Full source 
lemma zpow_sub_one₀ (ha : a ≠ 0) (n : ℤ) : a ^ (n - 1) = a ^ n * a⁻¹ :=
  calc
    a ^ (n - 1) = a ^ (n - 1) * a * a⁻¹ := by rw [mul_assoc, mul_inv_cancel₀ ha, mul_one]
    _ = a ^ n * a⁻¹ := by rw [← zpow_add_one₀ ha, Int.sub_add_cancel]
Power Subtraction Formula in Groups with Zero: $a^{n-1} = a^n \cdot a^{-1}$
Informal description
For any nonzero element $a$ in a group with zero $G_0$ and any integer $n$, the $(n-1)$-th power of $a$ equals the $n$-th power of $a$ multiplied by the inverse of $a$, i.e., $a^{n-1} = a^n \cdot a^{-1}$.
zpow_add₀ theorem
(ha : a ≠ 0) (m n : ℤ) : a ^ (m + n) = a ^ m * a ^ n
Full source 
lemma zpow_add₀ (ha : a ≠ 0) (m n : ℤ) : a ^ (m + n) = a ^ m * a ^ n := by
  induction n with
  | hz => simp
  | hp n ihn => simp only [← Int.add_assoc, zpow_add_one₀ ha, ihn, mul_assoc]
  | hn n ihn => rw [zpow_sub_one₀ ha, ← mul_assoc, ← ihn, ← zpow_sub_one₀ ha, Int.add_sub_assoc]
Exponent Addition Law for Groups with Zero: $a^{m+n} = a^m \cdot a^n$
Informal description
For any nonzero element $a$ in a group with zero $G_0$ and any integers $m, n$, the $(m+n)$-th power of $a$ equals the product of the $m$-th power and $n$-th power of $a$, i.e., $a^{m+n} = a^m \cdot a^n$.
zpow_add' theorem
{m n : ℤ} (h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0) : a ^ (m + n) = a ^ m * a ^ n
Full source 
lemma zpow_add' {m n : ℤ} (h : a ≠ 0a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0) :
    a ^ (m + n) = a ^ m * a ^ n := by
  by_cases hm : m = 0
  · simp [hm]
  by_cases hn : n = 0
  · simp [hn]
  by_cases ha : a = 0
  · subst a
    simp only [false_or, eq_self_iff_true, not_true, Ne, hm, hn, false_and, or_false] at h
    rw [zero_zpow _ h, zero_zpow _ hm, zero_mul]
  · exact zpow_add₀ ha m n
Exponent Addition Law for Groups with Zero under Non-Degenerate Conditions: $a^{m+n} = a^m \cdot a^n$
Informal description
For any element $a$ in a group with zero $G_0$ and any integers $m, n$, if either $a \neq 0$, or $m + n \neq 0$, or $m = 0$ and $n = 0$, then $a^{m+n} = a^m \cdot a^n$.
zpow_one_add₀ theorem
(h : a ≠ 0) (i : ℤ) : a ^ (1 + i) = a * a ^ i
Full source 
lemma zpow_one_add₀ (h : a ≠ 0) (i : ℤ) : a ^ (1 + i) = a * a ^ i := by rw [zpow_add₀ h, zpow_one]
Exponent Addition Identity for Groups with Zero: $a^{1 + i} = a \cdot a^i$
Informal description
For any nonzero element $a$ in a group with zero $G_0$ and any integer $i$, the $(1 + i)$-th power of $a$ equals the product of $a$ and the $i$-th power of $a$, i.e., $a^{1 + i} = a \cdot a^i$.
div_mul_eq_mul_div₀ theorem
(a b c : G₀) : a / c * b = a * b / c
Full source 
theorem div_mul_eq_mul_div₀ (a b c : G₀) : a / c * b = a * b / c := by
  simp_rw [div_eq_mul_inv, mul_assoc, mul_comm c⁻¹]
Division-Multiplication Commutativity in Groups with Zero: $(a / c) \cdot b = (a \cdot b) / c$
Informal description
For any elements $a$, $b$, and $c$ in a group with zero $G₀$, the following equality holds: $(a / c) \cdot b = (a \cdot b) / c$.
div_sq_cancel theorem
(a b : G₀) : a ^ 2 * b / a = a * b
Full source 
lemma div_sq_cancel (a b : G₀) : a ^ 2 * b / a = a * b := by
  obtain rfl | ha := eq_or_ne a 0
  · simp
  · rw [sq, mul_assoc, mul_div_cancel_left₀ _ ha]
Square Cancellation in Division for Groups with Zero: $a^2 b / a = a b$
Informal description
For any elements $a$ and $b$ in a group with zero $G_0$, the following equality holds: $a^2 \cdot b / a = a \cdot b$.