doc-next-gen

Mathlib.Algebra.GroupWithZero.Units.Basic

Module docstring

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

Units.ne_zero theorem
[Nontrivial M₀] (u : M₀ˣ) : (u : M₀) ≠ 0
Full source 
/-- An element of the unit group of a nonzero monoid with zero represented as an element
    of the monoid is nonzero. -/
@[simp]
theorem ne_zero [Nontrivial M₀] (u : M₀ˣ) : (u : M₀) ≠ 0 :=
  left_ne_zero_of_mul_eq_one u.mul_inv
Nonzero Property of Units in a Nontrivial Monoid with Zero
Informal description
In a nontrivial monoid with zero $M₀$, for any unit $u$ in the group of units $M₀^\times$, the element $u$ (considered as an element of $M₀$) is nonzero, i.e., $u \neq 0$.
Units.mul_left_eq_zero theorem
(u : M₀ˣ) {a : M₀} : a * u = 0 ↔ a = 0
Full source 
@[simp]
theorem mul_left_eq_zero (u : M₀ˣ) {a : M₀} : a * u = 0 ↔ a = 0 :=
  ⟨fun h => by simpa using mul_eq_zero_of_left h ↑u⁻¹, fun h => mul_eq_zero_of_left h u⟩
Left Multiplication by a Unit is Zero if and only if the Element is Zero
Informal description
For any unit $u$ in a monoid with zero $M₀$ and any element $a \in M₀$, the product $a \cdot u$ equals zero if and only if $a$ equals zero.
Units.mul_right_eq_zero theorem
(u : M₀ˣ) {a : M₀} : ↑u * a = 0 ↔ a = 0
Full source 
@[simp]
theorem mul_right_eq_zero (u : M₀ˣ) {a : M₀} : ↑u * a = 0 ↔ a = 0 :=
  ⟨fun h => by simpa using mul_eq_zero_of_right (↑u⁻¹) h, mul_eq_zero_of_right (u : M₀)⟩
Right Multiplication by a Unit is Zero if and only if the Element is Zero
Informal description
For any unit $u$ in a monoid with zero $M₀$ and any element $a \in M₀$, the product $u \cdot a$ equals zero if and only if $a$ equals zero.
IsUnit.ne_zero theorem
[Nontrivial M₀] {a : M₀} (ha : IsUnit a) : a ≠ 0
Full source 
theorem ne_zero [Nontrivial M₀] {a : M₀} (ha : IsUnit a) : a ≠ 0 :=
  let ⟨u, hu⟩ := ha
  hu ▸ u.ne_zero
Units are nonzero in a nontrivial monoid with zero
Informal description
In a nontrivial monoid with zero $M_0$, if an element $a \in M_0$ is a unit, then $a$ is nonzero, i.e., $a \neq 0$.
IsUnit.mul_right_eq_zero theorem
{a b : M₀} (ha : IsUnit a) : a * b = 0 ↔ b = 0
Full source 
theorem mul_right_eq_zero {a b : M₀} (ha : IsUnit a) : a * b = 0 ↔ b = 0 :=
  let ⟨u, hu⟩ := ha
  hu ▸ u.mul_right_eq_zero
Right Multiplication by a Unit is Zero if and only if the Element is Zero
Informal description
For any elements $a, b$ in a monoid with zero $M_0$, if $a$ is a unit, then the product $a \cdot b$ equals zero if and only if $b$ equals zero.
IsUnit.mul_left_eq_zero theorem
{a b : M₀} (hb : IsUnit b) : a * b = 0 ↔ a = 0
Full source 
theorem mul_left_eq_zero {a b : M₀} (hb : IsUnit b) : a * b = 0 ↔ a = 0 :=
  let ⟨u, hu⟩ := hb
  hu ▸ u.mul_left_eq_zero
$a \cdot b = 0 \leftrightarrow a = 0$ for $b$ a unit in a monoid with zero
Informal description
For any elements $a, b$ in a monoid with zero $M_0$, if $b$ is a unit, then the product $a \cdot b$ equals zero if and only if $a$ equals zero.
isUnit_zero_iff theorem
: IsUnit (0 : M₀) ↔ (0 : M₀) = 1
Full source 
@[simp]
theorem isUnit_zero_iff : IsUnitIsUnit (0 : M₀) ↔ (0 : M₀) = 1 :=
  ⟨fun ⟨⟨_, a, (a0 : 0 * a = 1), _⟩, rfl⟩ => by rwa [zero_mul] at a0, fun h =>
    @isUnit_of_subsingleton _ _ (subsingleton_of_zero_eq_one h) 0⟩
Zero is a Unit if and only if Zero Equals One in a Monoid with Zero
Informal description
In a monoid with zero $M_0$, the zero element $0$ is a unit if and only if $0$ is equal to the multiplicative identity $1$.
Ring.inverse definition
: M₀ → M₀
Full source 
/-- 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₀`. -/
noncomputable def inverse : M₀ → M₀ := fun x => if h : IsUnit x then ((h.unit⁻¹ : M₀ˣ) : M₀) else 0
Inverse function on a monoid with zero
Informal description
The function `inverse` on a monoid with zero `M₀` sends an element `x` to its multiplicative inverse `x⁻¹` if `x` is a unit (i.e., invertible), and to `0` otherwise. Formally, for any `x ∈ M₀`, \[ \text{inverse}(x) = \begin{cases} x^{-1} & \text{if } x \text{ is a unit}, \\ 0 & \text{otherwise}. \end{cases} \] This function is fully defined (rather than partially defined) for convenience in applications such as calculus.
Ring.inverse_unit theorem
(u : M₀ˣ) : inverse (u : M₀) = (u⁻¹ : M₀ˣ)
Full source 
/-- By definition, if `x` is invertible then `inverse x = x⁻¹`. -/
@[simp]
theorem inverse_unit (u : M₀ˣ) : inverse (u : M₀) = (u⁻¹ : M₀ˣ) := by
  rw [inverse, dif_pos u.isUnit, IsUnit.unit_of_val_units]
Inverse of a Unit Equals Its Multiplicative Inverse
Informal description
For any unit $u$ in a monoid with zero $M_0$, the inverse function satisfies $\text{inverse}(u) = u^{-1}$.
Ring.inverse_of_isUnit theorem
{x : M₀} (h : IsUnit x) : inverse x = ((h.unit⁻¹ : M₀ˣ) : M₀)
Full source 
theorem inverse_of_isUnit {x : M₀} (h : IsUnit x) : inverse x = ((h.unit⁻¹ : M₀ˣ) : M₀) := dif_pos h
Ring Inverse of a Unit Equals Its Group Inverse
Informal description
For any element $x$ in a monoid with zero $M_0$, if $x$ is a unit (i.e., invertible), then the ring inverse of $x$ equals the inverse of the corresponding unit element in the group of units $M_0^\times$, i.e., \[ \text{inverse}(x) = (h.\text{unit})^{-1}, \] where $h.\text{unit}$ is the unit element corresponding to $x$ under the proof $h$ that $x$ is a unit.
Ring.inverse_non_unit theorem
(x : M₀) (h : ¬IsUnit x) : inverse x = 0
Full source 
/-- By definition, if `x` is not invertible then `inverse x = 0`. -/
@[simp]
theorem inverse_non_unit (x : M₀) (h : ¬IsUnit x) : inverse x = 0 :=
  dif_neg h
Inverse of Non-Unit is Zero in Monoid with Zero
Informal description
For any element $x$ in a monoid with zero $M_0$ that is not a unit, the inverse function satisfies $\text{inverse}(x) = 0$.
Ring.mul_inverse_cancel theorem
(x : M₀) (h : IsUnit x) : x * inverse x = 1
Full source 
theorem mul_inverse_cancel (x : M₀) (h : IsUnit x) : x * inverse x = 1 := by
  rcases h with ⟨u, rfl⟩
  rw [inverse_unit, Units.mul_inv]
Product of Unit and Its Ring Inverse Equals One
Informal description
For any element $x$ in a monoid with zero $M_0$, if $x$ is a unit (i.e., invertible), then the product of $x$ and its ring inverse equals the multiplicative identity, i.e., $x \cdot \text{inverse}(x) = 1$.
Ring.inverse_mul_cancel theorem
(x : M₀) (h : IsUnit x) : inverse x * x = 1
Full source 
theorem inverse_mul_cancel (x : M₀) (h : IsUnit x) : inverse x * x = 1 := by
  rcases h with ⟨u, rfl⟩
  rw [inverse_unit, Units.inv_mul]
Left Cancellation Property for the Inverse Function in a Monoid with Zero
Informal description
For any element $x$ in a monoid with zero $M_0$ that is a unit, the product of the inverse function applied to $x$ and $x$ itself equals the multiplicative identity, i.e., $\text{inverse}(x) \cdot x = 1$.
Ring.mul_inverse_cancel_right theorem
(x y : M₀) (h : IsUnit x) : y * x * inverse x = y
Full source 
theorem mul_inverse_cancel_right (x y : M₀) (h : IsUnit x) : y * x * inverse x = y := by
  rw [mul_assoc, mul_inverse_cancel x h, mul_one]
Right Cancellation Property for the Inverse Function in a Monoid with Zero
Informal description
For any elements $x$ and $y$ in a monoid with zero $M_0$, if $x$ is a unit, then the product $y \cdot x \cdot \text{inverse}(x)$ equals $y$.
Ring.inverse_mul_cancel_right theorem
(x y : M₀) (h : IsUnit x) : y * inverse x * x = y
Full source 
theorem inverse_mul_cancel_right (x y : M₀) (h : IsUnit x) : y * inverse x * x = y := by
  rw [mul_assoc, inverse_mul_cancel x h, mul_one]
Right Cancellation Property for the Inverse Function in a Monoid with Zero
Informal description
For any elements $x$ and $y$ in a monoid with zero $M_0$, if $x$ is a unit, then $y \cdot \text{inverse}(x) \cdot x = y$.
Ring.mul_inverse_cancel_left theorem
(x y : M₀) (h : IsUnit x) : x * (inverse x * y) = y
Full source 
theorem mul_inverse_cancel_left (x y : M₀) (h : IsUnit x) : x * (inverse x * y) = y := by
  rw [← mul_assoc, mul_inverse_cancel x h, one_mul]
Left Cancellation Property for Ring Inverse
Informal description
For any elements $x$ and $y$ in a monoid with zero $M_0$, if $x$ is a unit, then $x \cdot (\text{inverse}(x) \cdot y) = y$.
Ring.inverse_mul_cancel_left theorem
(x y : M₀) (h : IsUnit x) : inverse x * (x * y) = y
Full source 
theorem inverse_mul_cancel_left (x y : M₀) (h : IsUnit x) : inverse x * (x * y) = y := by
  rw [← mul_assoc, inverse_mul_cancel x h, one_mul]
Left Cancellation Property for the Inverse Function in a Monoid with Zero
Informal description
For any elements $x$ and $y$ in a monoid with zero $M_0$, if $x$ is a unit, then the product of the inverse of $x$ with the product of $x$ and $y$ equals $y$, i.e., $\text{inverse}(x) \cdot (x \cdot y) = y$.
Ring.inverse_mul_eq_iff_eq_mul theorem
(x y z : M₀) (h : IsUnit x) : inverse x * y = z ↔ y = x * z
Full source 
theorem inverse_mul_eq_iff_eq_mul (x y z : M₀) (h : IsUnit x) : inverseinverse x * y = z ↔ y = x * z :=
  ⟨fun h1 => by rw [← h1, mul_inverse_cancel_left _ _ h],
  fun h1 => by rw [h1, inverse_mul_cancel_left _ _ h]⟩
Equivalence of Inverse Multiplication and Multiplication in a Monoid with Zero
Informal description
For any elements $x$, $y$, and $z$ in a monoid with zero $M_0$, if $x$ is a unit, then the equation $\text{inverse}(x) \cdot y = z$ holds if and only if $y = x \cdot z$.
Ring.inverse_one theorem
: inverse (1 : M₀) = 1
Full source 
@[simp]
theorem inverse_one : inverse (1 : M₀) = 1 :=
  inverse_unit 1
Inverse of the Identity Element is the Identity
Informal description
The inverse function evaluated at the multiplicative identity $1$ in a monoid with zero $M_0$ returns $1$, i.e., $\text{inverse}(1) = 1$.
Ring.inverse_zero theorem
: inverse (0 : M₀) = 0
Full source 
@[simp]
theorem inverse_zero : inverse (0 : M₀) = 0 := by
  nontriviality
  exact inverse_non_unit _ not_isUnit_zero
Inverse of Zero is Zero in Monoid with Zero
Informal description
In any monoid with zero $M_0$, the inverse function evaluated at the zero element equals zero, i.e., $\text{inverse}(0) = 0$.
IsUnit.ringInverse theorem
{a : M₀} : IsUnit a → IsUnit (Ring.inverse a)
Full source 
theorem IsUnit.ringInverse {a : M₀} : IsUnit a → IsUnit (Ring.inverse a)
  | ⟨u, hu⟩ => hu ▸ ⟨u⁻¹, (Ring.inverse_unit u).symm⟩
Inverse of a Unit is a Unit
Informal description
For any element $a$ in a monoid with zero $M_0$, if $a$ is a unit (i.e., invertible), then its inverse under the `Ring.inverse` function is also a unit.
isUnit_ringInverse theorem
{a : M₀} : IsUnit (Ring.inverse a) ↔ IsUnit a
Full source 
@[simp]
theorem isUnit_ringInverse {a : M₀} : IsUnitIsUnit (Ring.inverse a) ↔ IsUnit a :=
  ⟨fun h => by
    cases subsingleton_or_nontrivial M₀
    · convert h
    · contrapose h
      rw [Ring.inverse_non_unit _ h]
      exact not_isUnit_zero
      ,
    IsUnit.ringInverse⟩
Inverse is Unit if and only if Element is Unit in Monoid with Zero
Informal description
For any element $a$ in a monoid with zero $M_0$, the inverse $\text{inverse}(a)$ is a unit if and only if $a$ itself is a unit.
Units.mk0 definition
(a : G₀) (ha : a ≠ 0) : G₀ˣ
Full source 
/-- 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. -/
def mk0 (a : G₀) (ha : a ≠ 0) : G₀ˣ :=
  ⟨a, a⁻¹, mul_inv_cancel₀ ha, inv_mul_cancel₀ ha⟩
Embedding of nonzero elements into the group of units
Informal description
Given a group with zero $G_0$ and a nonzero element $a \in G_0$, the function `Units.mk0` constructs a unit element in the group of units $G_0^\times$ by pairing $a$ with its multiplicative inverse $a^{-1}$. This ensures that $a \cdot a^{-1} = 1$ and $a^{-1} \cdot a = 1$, making $a$ invertible in $G_0^\times$.
Units.val_mk0 theorem
{a : G₀} (h : a ≠ 0) : (mk0 a h : G₀) = a
Full source 
@[simp]
theorem val_mk0 {a : G₀} (h : a ≠ 0) : (mk0 a h : G₀) = a :=
  rfl
Embedding of Nonzero Elements Preserves Value
Informal description
For any nonzero element $a$ in a group with zero $G_0$, the underlying value of the unit element constructed via `Units.mk0 a h` is equal to $a$ itself. That is, if $a \neq 0$, then $(\text{Units.mk0}\ a\ h : G_0) = a$.
Units.mk0_val theorem
(u : G₀ˣ) (h : (u : G₀) ≠ 0) : mk0 (u : G₀) h = u
Full source 
@[simp]
theorem mk0_val (u : G₀ˣ) (h : (u : G₀) ≠ 0) : mk0 (u : G₀) h = u :=
  Units.ext rfl
Reconstruction of Unit from Its Underlying Nonzero Element
Informal description
For any unit $u$ in the group of units $G_0^\times$ of a group with zero $G_0$, if the underlying element $(u : G_0)$ is nonzero, then constructing a unit from $(u : G_0)$ using `Units.mk0` returns $u$ itself. In other words, $\text{mk0}(u, h) = u$ where $h$ is the proof that $(u : G_0) \neq 0$.
Units.mul_inv' theorem
(u : G₀ˣ) : u * (u : G₀)⁻¹ = 1
Full source 
theorem mul_inv' (u : G₀ˣ) : u * (u : G₀)⁻¹ = 1 :=
  mul_inv_cancel₀ u.ne_zero
Unit Multiplied by Inverse of Underlying Element Equals One
Informal description
For any unit $u$ in the group of units $G_0^\times$ of a group with zero $G_0$, the product of $u$ and the inverse of its underlying element in $G_0$ equals the multiplicative identity, i.e., $u \cdot (u : G_0)^{-1} = 1$.
Units.inv_mul' theorem
(u : G₀ˣ) : (u⁻¹ : G₀) * u = 1
Full source 
theorem inv_mul' (u : G₀ˣ) : (u⁻¹ : G₀) * u = 1 :=
  inv_mul_cancel₀ u.ne_zero
Inverse-Unit Multiplication Identity in Group with Zero
Informal description
For any unit $u$ in the group of units $G_0^\times$ of a group with zero $G_0$, the product of the inverse of $u$ (considered as an element of $G_0$) and $u$ itself equals the multiplicative identity, i.e., $u^{-1} \cdot u = 1$.
Units.mk0_inj theorem
{a b : G₀} (ha : a ≠ 0) (hb : b ≠ 0) : Units.mk0 a ha = Units.mk0 b hb ↔ a = b
Full source 
@[simp]
theorem mk0_inj {a b : G₀} (ha : a ≠ 0) (hb : b ≠ 0) : Units.mk0Units.mk0 a ha = Units.mk0 b hb ↔ a = b :=
  ⟨fun h => by injection h, fun h => Units.ext h⟩
Injectivity of Unit Construction from Nonzero Elements in a Group with Zero
Informal description
For any nonzero elements $a$ and $b$ in a group with zero $G_0$, the units constructed via `Units.mk0` are equal if and only if the original elements are equal. That is, $\text{Units.mk0}(a, h_a) = \text{Units.mk0}(b, h_b) \leftrightarrow a = b$, where $h_a$ and $h_b$ are proofs that $a \neq 0$ and $b \neq 0$ respectively.
Units.exists0 theorem
{p : G₀ˣ → Prop} : (∃ g : G₀ˣ, p g) ↔ ∃ (g : G₀) (hg : g ≠ 0), p (Units.mk0 g hg)
Full source 
/-- In a group with zero, an existential over a unit can be rewritten in terms of `Units.mk0`. -/
theorem exists0 {p : G₀ˣ → Prop} : (∃ g : G₀ˣ, p g) ↔ ∃ (g : G₀) (hg : g ≠ 0), p (Units.mk0 g hg) :=
  ⟨fun ⟨g, pg⟩ => ⟨g, g.ne_zero, (g.mk0_val g.ne_zero).symm ▸ pg⟩,
  fun ⟨g, hg, pg⟩ => ⟨Units.mk0 g hg, pg⟩⟩
Existence of Unit Satisfying Predicate is Equivalent to Existence of Nonzero Element Satisfying Predicate via `Units.mk0`
Informal description
For any predicate $p$ on the group of units $G_0^\times$ of a group with zero $G_0$, there exists a unit $g \in G_0^\times$ satisfying $p(g)$ if and only if there exists a nonzero element $g \in G_0$ (with proof $hg : g \neq 0$) such that $p(\text{Units.mk0}(g, hg))$ holds.
Units.exists0' theorem
{p : ∀ g : G₀, g ≠ 0 → Prop} : (∃ (g : G₀) (hg : g ≠ 0), p g hg) ↔ ∃ g : G₀ˣ, p g g.ne_zero
Full source 
/-- An alternative version of `Units.exists0`. This one is useful if Lean cannot
figure out `p` when using `Units.exists0` from right to left. -/
theorem exists0' {p : ∀ g : G₀, g ≠ 0 → Prop} :
    (∃ (g : G₀) (hg : g ≠ 0), p g hg) ↔ ∃ g : G₀ˣ, p g g.ne_zero :=
  Iff.trans (by simp_rw [val_mk0]) exists0.symm
Existence of Nonzero Element Satisfying Predicate is Equivalent to Existence of Unit Satisfying Predicate via `Units.ne_zero`
Informal description
For any predicate $p$ on the nonzero elements of a group with zero $G_0$, there exists a nonzero element $g \in G_0$ (with proof $hg : g \neq 0$) such that $p(g, hg)$ holds if and only if there exists a unit $g \in G_0^\times$ such that $p(g, g.\text{ne\_zero})$ holds.
Units.exists_iff_ne_zero theorem
{p : G₀ → Prop} : (∃ u : G₀ˣ, p u) ↔ ∃ x ≠ 0, p x
Full source 
@[simp]
theorem exists_iff_ne_zero {p : G₀ → Prop} : (∃ u : G₀ˣ, p u) ↔ ∃ x ≠ 0, p x := by
  simp [exists0]
Existence of Units in a Group with Zero is Equivalent to Existence of Nonzero Elements Satisfying a Predicate
Informal description
For any predicate $p$ on a group with zero $G_0$, there exists a unit $u \in G_0^\times$ such that $p(u)$ holds if and only if there exists a nonzero element $x \in G_0$ such that $p(x)$ holds.
IsUnit.mk0 theorem
(x : G₀) (hx : x ≠ 0) : IsUnit x
Full source 
theorem IsUnit.mk0 (x : G₀) (hx : x ≠ 0) : IsUnit x :=
  (Units.mk0 x hx).isUnit
Nonzero Elements are Units in a Group with Zero
Informal description
For any element $x$ in a group with zero $G_0$, if $x$ is nonzero, then $x$ is a unit (i.e., invertible).
isUnit_iff_ne_zero theorem
: IsUnit a ↔ a ≠ 0
Full source 
@[simp]
theorem isUnit_iff_ne_zero : IsUnitIsUnit a ↔ a ≠ 0 :=
  (Units.exists_iff_ne_zero (p := (· = a))).trans (by simp)
Characterization of Units in a Group with Zero: $a$ is a unit $\leftrightarrow$ $a \neq 0$
Informal description
An element $a$ in a group with zero $G_0$ is a unit if and only if $a$ is nonzero.
GroupWithZero.noZeroDivisors instance
: NoZeroDivisors G₀
Full source 
instance (priority := 10) GroupWithZero.noZeroDivisors : NoZeroDivisors G₀ :=
  { (‹_› : GroupWithZero G₀) with
    eq_zero_or_eq_zero_of_mul_eq_zero := @fun a b h => by
      contrapose! h
      exact (Units.mk0 a h.1 * Units.mk0 b h.2).ne_zero }
Groups with Zero Have No Zero Divisors
Informal description
Every group with zero $G_0$ has no zero divisors. That is, for any elements $a, b \in G_0$, if $a \cdot b = 0$, then either $a = 0$ or $b = 0$.
Units.mk0_mul theorem
(x y : G₀) (hxy) : Units.mk0 (x * y) hxy = Units.mk0 x (mul_ne_zero_iff.mp hxy).1 * Units.mk0 y (mul_ne_zero_iff.mp hxy).2
Full source 
@[simp]
theorem Units.mk0_mul (x y : G₀) (hxy) :
    Units.mk0 (x * y) hxy =
      Units.mk0 x (mul_ne_zero_iff.mp hxy).1 * Units.mk0 y (mul_ne_zero_iff.mp hxy).2 := by
  ext; rfl
Multiplicativity of Unit Construction in a Group with Zero
Informal description
Let $G_0$ be a group with zero, and let $x, y \in G_0$ be nonzero elements such that their product $x \cdot y$ is also nonzero. Then the unit constructed from $x \cdot y$ is equal to the product of the units constructed from $x$ and $y$ individually. That is, \[ \text{Units.mk0}(x \cdot y, hxy) = \text{Units.mk0}(x, hx) \cdot \text{Units.mk0}(y, hy), \] where $hx$ and $hy$ are the proofs that $x \neq 0$ and $y \neq 0$ respectively, derived from $hxy$ via the condition that a product is nonzero if and only if both factors are nonzero.
div_ne_zero theorem
(ha : a ≠ 0) (hb : b ≠ 0) : a / b ≠ 0
Full source 
theorem div_ne_zero (ha : a ≠ 0) (hb : b ≠ 0) : a / b ≠ 0 := by
  rw [div_eq_mul_inv]
  exact mul_ne_zero ha (inv_ne_zero hb)
Nonzero Elements Divide 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 quotient $a / b \neq 0$.
div_eq_zero_iff theorem
: a / b = 0 ↔ a = 0 ∨ b = 0
Full source 
@[simp]
theorem div_eq_zero_iff : a / b = 0 ↔ a = 0 ∨ b = 0 := by simp [div_eq_mul_inv]
Division Equals Zero if and only if Either Operand is Zero
Informal description
For any elements $a$ and $b$ in a group with zero, the division $a / b$ equals zero if and only if either $a$ is zero or $b$ is zero.
div_self theorem
(h : a ≠ 0) : a / a = 1
Full source 
@[simp] lemma div_self (h : a ≠ 0) : a / a = 1 := h.isUnit.div_self
Division of Nonzero Element by Itself Yields Identity
Informal description
For any nonzero element $a$ in a group with zero, the division of $a$ by itself yields the multiplicative identity, i.e., $a / a = 1$.
mul_inv_eq_iff_eq_mul₀ theorem
(hb : b ≠ 0) : a * b⁻¹ = c ↔ a = c * b
Full source 
lemma mul_inv_eq_iff_eq_mul₀ (hb : b ≠ 0) : a * b⁻¹ = c ↔ a = c * b :=
  hb.isUnit.mul_inv_eq_iff_eq_mul
Equivalence of right multiplication by inverse and original multiplication for nonzero elements: $a \cdot b^{-1} = c \leftrightarrow a = c \cdot b$
Informal description
For any elements $a$, $b$, and $c$ in a group with zero, if $b$ is nonzero, then $a \cdot b^{-1} = c$ if and only if $a = c \cdot b$.
mul_inv_eq_one₀ theorem
(hb : b ≠ 0) : a * b⁻¹ = 1 ↔ a = b
Full source 
lemma mul_inv_eq_one₀ (hb : b ≠ 0) : a * b⁻¹ = 1 ↔ a = b := hb.isUnit.mul_inv_eq_one
Inverse Condition: $a \cdot b^{-1} = 1 \leftrightarrow a = b$ for nonzero $b$
Informal description
For any elements $a$ and $b$ in a group with zero, if $b$ is nonzero, then $a \cdot b^{-1} = 1$ if and only if $a = b$.
inv_mul_eq_one₀ theorem
(ha : a ≠ 0) : a⁻¹ * b = 1 ↔ a = b
Full source 
lemma inv_mul_eq_one₀ (ha : a ≠ 0) : a⁻¹a⁻¹ * b = 1 ↔ a = b := ha.isUnit.inv_mul_eq_one
Inverse Multiplication Condition in Groups with Zero: $a^{-1} \cdot b = 1 \leftrightarrow a = b$ for $a \neq 0$
Informal description
For any elements $a$ and $b$ in a group with zero, if $a$ is nonzero, then the product $a^{-1} \cdot b$ equals $1$ if and only if $a = b$.
mul_eq_one_iff_eq_inv₀ theorem
(hb : b ≠ 0) : a * b = 1 ↔ a = b⁻¹
Full source 
lemma mul_eq_one_iff_eq_inv₀ (hb : b ≠ 0) : a * b = 1 ↔ a = b⁻¹ := hb.isUnit.mul_eq_one_iff_eq_inv
Inverse Characterization in Groups with Zero: $a \cdot b = 1 \leftrightarrow a = b^{-1}$ for $b \neq 0$
Informal description
For any elements $a$ and $b$ in a group with zero $G_0$, if $b$ is nonzero, then the product $a \cdot b$ equals the multiplicative identity $1$ if and only if $a$ is equal to the inverse of $b$, i.e., $a \cdot b = 1 \leftrightarrow a = b^{-1}$.
mul_eq_one_iff_inv_eq₀ theorem
(ha : a ≠ 0) : a * b = 1 ↔ a⁻¹ = b
Full source 
lemma mul_eq_one_iff_inv_eq₀ (ha : a ≠ 0) : a * b = 1 ↔ a⁻¹ = b := ha.isUnit.mul_eq_one_iff_inv_eq
Inverse Characterization in Group with Zero: $a \cdot b = 1 \leftrightarrow a^{-1} = b$ for $a \neq 0$
Informal description
For any nonzero elements $a$ and $b$ in a group with zero, the product $a \cdot b$ equals $1$ if and only if the inverse of $a$ equals $b$, i.e., $a \cdot b = 1 \leftrightarrow a^{-1} = b$.
mul_eq_of_eq_mul_inv₀ theorem
(ha : a ≠ 0) (h : a = c * b⁻¹) : a * b = c
Full source 
/-- A variant of `eq_mul_inv_iff_mul_eq₀` that moves the nonzero hypothesis to another variable. -/
lemma mul_eq_of_eq_mul_inv₀ (ha : a ≠ 0) (h : a = c * b⁻¹) : a * b = c := by
  rwa [← eq_mul_inv_iff_mul_eq₀]; rintro rfl; simp [ha] at h
Multiplication by Inverse in Group with Zero: $a = c \cdot b^{-1} \Rightarrow a \cdot b = c$
Informal description
Let $G₀$ be a group with zero. For any nonzero elements $a, b, c \in G₀$, if $a = c \cdot b^{-1}$, then $a \cdot b = c$.
mul_eq_of_eq_inv_mul₀ theorem
(hb : b ≠ 0) (h : b = a⁻¹ * c) : a * b = c
Full source 
/-- A variant of `eq_inv_mul_iff_mul_eq₀` that moves the nonzero hypothesis to another variable. -/
lemma mul_eq_of_eq_inv_mul₀ (hb : b ≠ 0) (h : b = a⁻¹ * c) : a * b = c := by
  rwa [← eq_inv_mul_iff_mul_eq₀]; rintro rfl; simp [hb] at h
Multiplication by Inverse in a Group with Zero
Informal description
Let $G₀$ be a group with zero, and let $a, b, c \in G₀$ such that $b \neq 0$. If $b = a^{-1} * c$, then $a * b = c$.
div_mul_cancel₀ theorem
(a : G₀) (h : b ≠ 0) : a / b * b = a
Full source 
@[simp] lemma div_mul_cancel₀ (a : G₀) (h : b ≠ 0) : a / b * b = a := h.isUnit.div_mul_cancel _
Right Cancellation Property for Division by Nonzero Elements: $(a / b) \cdot b = a$
Informal description
For any element $a$ in a group with zero $G_0$ and any nonzero element $b \in G_0$, the expression $(a / b) \cdot b$ simplifies to $a$.
mul_one_div_cancel theorem
(h : a ≠ 0) : a * (1 / a) = 1
Full source 
lemma mul_one_div_cancel (h : a ≠ 0) : a * (1 / a) = 1 := h.isUnit.mul_one_div_cancel
Multiplicative Inverse Property: $a \cdot (1/a) = 1$ for $a \neq 0$
Informal description
For any nonzero element $a$ in a group with zero $G_0$, the product of $a$ and its multiplicative inverse $1/a$ equals the multiplicative identity, i.e., $a \cdot (1/a) = 1$.
one_div_mul_cancel theorem
(h : a ≠ 0) : 1 / a * a = 1
Full source 
lemma one_div_mul_cancel (h : a ≠ 0) : 1 / a * a = 1 := h.isUnit.one_div_mul_cancel
Inverse Property for Nonzero Elements: $\frac{1}{a} \cdot a = 1$
Informal description
For any nonzero element $a$ in a group with zero, the product of its multiplicative inverse and itself equals the multiplicative identity, i.e., $\frac{1}{a} \cdot a = 1$.
div_left_inj' theorem
(hc : c ≠ 0) : a / c = b / c ↔ a = b
Full source 
lemma div_left_inj' (hc : c ≠ 0) : a / c = b / c ↔ a = b := hc.isUnit.div_left_inj
Left Cancellation Property for Division by Nonzero Elements: $a / c = b / c \leftrightarrow a = b$
Informal description
For any nonzero element $c$ in a group with zero, the equality $a / c = b / c$ holds if and only if $a = b$.
div_eq_iff theorem
(hb : b ≠ 0) : a / b = c ↔ a = c * b
Full source 
@[field_simps] lemma div_eq_iff (hb : b ≠ 0) : a / b = c ↔ a = c * b := hb.isUnit.div_eq_iff
Division Equivalence: $a / b = c \leftrightarrow a = c \cdot b$ for $b \neq 0$
Informal description
For any nonzero element $b$ in a group with zero, the equation $a / b = c$ holds if and only if $a = c \cdot b$.
div_eq_iff_mul_eq theorem
(hb : b ≠ 0) : a / b = c ↔ c * b = a
Full source 
lemma div_eq_iff_mul_eq (hb : b ≠ 0) : a / b = c ↔ c * b = a := hb.isUnit.div_eq_iff.trans eq_comm
Division Equivalence: $a / b = c \leftrightarrow c \cdot b = a$ for $b \neq 0$
Informal description
For any elements $a$, $b$, and $c$ in a group with zero, if $b \neq 0$, then $a / b = c$ if and only if $c \cdot b = a$.
div_eq_of_eq_mul theorem
(hb : b ≠ 0) : a = c * b → a / b = c
Full source 
lemma div_eq_of_eq_mul (hb : b ≠ 0) : a = c * b → a / b = c := hb.isUnit.div_eq_of_eq_mul
Division by Nonzero Element Equals Multiplicative Factor: $a = c \cdot b \rightarrow a / b = c$
Informal description
For any elements $a$, $b$, and $c$ in a group with zero, if $b$ is nonzero and $a = c \cdot b$, then $a / b = c$.
div_eq_one_iff_eq theorem
(hb : b ≠ 0) : a / b = 1 ↔ a = b
Full source 
lemma div_eq_one_iff_eq (hb : b ≠ 0) : a / b = 1 ↔ a = b := hb.isUnit.div_eq_one_iff_eq
Division by Nonzero Element Equals One iff Elements Are Equal
Informal description
For any elements $a$ and $b$ in a group with zero $G_0$, where $b$ is nonzero, the equation $a / b = 1$ holds if and only if $a = b$.
div_mul_cancel_right₀ theorem
(hb : b ≠ 0) (a : G₀) : b / (a * b) = a⁻¹
Full source 
lemma div_mul_cancel_right₀ (hb : b ≠ 0) (a : G₀) : b / (a * b) = a⁻¹ :=
  hb.isUnit.div_mul_cancel_right _
Right Cancellation Property for Nonzero Elements: $b / (a \cdot b) = a^{-1}$
Informal description
For any nonzero element $b$ in a group with zero $G_0$ and any element $a \in G_0$, the following holds: \[ b / (a \cdot b) = a^{-1}. \]
mul_div_mul_right theorem
(a b : G₀) (hc : c ≠ 0) : a * c / (b * c) = a / b
Full source 
lemma mul_div_mul_right (a b : G₀) (hc : c ≠ 0) : a * c / (b * c) = a / b :=
  hc.isUnit.mul_div_mul_right _ _
Right Cancellation Property for Nonzero Elements: $(a \cdot c) / (b \cdot c) = a / b$
Informal description
For any elements $a, b, c$ in a group with zero $G_0$, if $c$ is nonzero, then the following equality holds: \[ (a \cdot c) / (b \cdot c) = a / b. \]
mul_mul_div theorem
(a : G₀) (hb : b ≠ 0) : a = a * b * (1 / b)
Full source 
lemma mul_mul_div (a : G₀) (hb : b ≠ 0) : a = a * b * (1 / b) := (hb.isUnit.mul_mul_div _).symm
Simplification Identity: $a = a \cdot b \cdot (1/b)$ for $b \neq 0$
Informal description
For any element $a$ in a group with zero $G_0$ and any nonzero element $b \in G_0$, the expression $a \cdot b \cdot (1 / b)$ simplifies to $a$, i.e., $a = a \cdot b \cdot (1 / b)$.
div_div_div_cancel_right₀ theorem
(hc : c ≠ 0) (a b : G₀) : a / c / (b / c) = a / b
Full source 
lemma div_div_div_cancel_right₀ (hc : c ≠ 0) (a b : G₀) : a / c / (b / c) = a / b := by
  rw [div_div_eq_mul_div, div_mul_cancel₀ _ hc]
Division Cancellation Identity: $\frac{a/c}{b/c} = a/b$ for $c \neq 0$
Informal description
For any elements $a$, $b$ in a group with zero $G_0$ and any nonzero element $c \in G_0$, the following equality holds: $$ \frac{a/c}{b/c} = \frac{a}{b} $$
div_mul_div_cancel₀ theorem
(hb : b ≠ 0) : a / b * (b / c) = a / c
Full source 
lemma div_mul_div_cancel₀ (hb : b ≠ 0) : a / b * (b / c) = a / c := by
  rw [← mul_div_assoc, div_mul_cancel₀ _ hb]
Fraction Cancellation Identity: $(a/b) \cdot (b/c) = a/c$ for $b \neq 0$
Informal description
For any elements $a, b, c$ in a group with zero $G_0$, if $b \neq 0$, then $(a / b) \cdot (b / c) = a / c$.
div_mul_cancel_of_imp theorem
(h : b = 0 → a = 0) : a / b * b = a
Full source 
lemma div_mul_cancel_of_imp (h : b = 0 → a = 0) : a / b * b = a := by
  obtain rfl | hb := eq_or_ne b 0 <;>  simp [*]
Conditional Right Cancellation Property for Division in Groups with Zero: $(a / b) \cdot b = a$ when $b = 0 \Rightarrow a = 0$
Informal description
For any elements $a$ and $b$ in a group with zero $G_0$, if $b = 0$ implies $a = 0$, then $(a / b) \cdot b = a$.
mul_div_cancel_of_imp theorem
(h : b = 0 → a = 0) : a * b / b = a
Full source 
lemma mul_div_cancel_of_imp (h : b = 0 → a = 0) : a * b / b = a := by
  obtain rfl | hb := eq_or_ne b 0 <;>  simp [*]
Cancellation Property for Multiplication and Division in Groups with Zero: $a \cdot b / b = a$ under Implication Condition
Informal description
For any elements $a$ and $b$ in a group with zero, if $b = 0$ implies $a = 0$, then $a \cdot b / b = a$.
divp_mk0 theorem
(a : G₀) (hb : b ≠ 0) : a /ₚ Units.mk0 b hb = a / b
Full source 
@[simp] lemma divp_mk0 (a : G₀) (hb : b ≠ 0) : a /ₚ Units.mk0 b hb = a / b := divp_eq_div _ _
Division by Unit Construction: $a /ₚ \text{Units.mk0}\, b\, hb = a / b$
Informal description
For any element $a$ in a group with zero $G_0$ and any nonzero element $b \in G_0$, the division operation $a /ₚ u$ (where $u = \text{Units.mk0}\, b\, hb$ is the unit constructed from $b$) is equal to the standard division $a / b$.
pow_sub₀ theorem
(a : G₀) (ha : a ≠ 0) (h : n ≤ m) : a ^ (m - n) = a ^ m * (a ^ n)⁻¹
Full source 
lemma pow_sub₀ (a : G₀) (ha : a ≠ 0) (h : n ≤ m) : a ^ (m - n) = a ^ m * (a ^ n)⁻¹ := by
  have h1 : m - n + n = m := Nat.sub_add_cancel h
  have h2 : a ^ (m - n) * a ^ n = a ^ m := by rw [← pow_add, h1]
  simpa only [div_eq_mul_inv] using eq_div_of_mul_eq (pow_ne_zero _ ha) h2
Power Subtraction Law in Groups with Zero: $a^{m-n} = a^m \cdot (a^n)^{-1}$ for $a \neq 0$ and $n \leq m$
Informal description
For any nonzero element $a$ in a group with zero $G_0$ and natural numbers $m$ and $n$ such that $n \leq m$, the power of $a$ raised to $m - n$ equals the product of $a^m$ and the inverse of $a^n$, i.e., $a^{m - n} = a^m \cdot (a^n)^{-1}$.
pow_sub_of_lt theorem
(a : G₀) (h : n < m) : a ^ (m - n) = a ^ m * (a ^ n)⁻¹
Full source 
lemma pow_sub_of_lt (a : G₀) (h : n < m) : a ^ (m - n) = a ^ m * (a ^ n)⁻¹ := by
  obtain rfl | ha := eq_or_ne a 0
  · rw [zero_pow (Nat.ne_of_gt <| Nat.sub_pos_of_lt h), zero_pow (by omega), zero_mul]
  · exact pow_sub₀ _ ha <| Nat.le_of_lt h
Power Subtraction Law for $n < m$: $a^{m-n} = a^m \cdot (a^n)^{-1}$ in Groups with Zero
Informal description
For any element $a$ in a group with zero $G_0$ and natural numbers $n$ and $m$ such that $n < m$, the power of $a$ raised to $m - n$ equals the product of $a^m$ and the inverse of $a^n$, i.e., $a^{m - n} = a^m \cdot (a^n)^{-1}$.
inv_pow_sub₀ theorem
(ha : a ≠ 0) (h : n ≤ m) : a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
Full source 
lemma inv_pow_sub₀ (ha : a ≠ 0) (h : n ≤ m) : a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n := by
  rw [pow_sub₀ _ (inv_ne_zero ha) h, inv_pow, inv_pow, inv_inv]
Inverse Power Subtraction Law: $(a^{-1})^{m-n} = (a^m)^{-1} \cdot a^n$ for $a \neq 0$ and $n \leq m$
Informal description
For any nonzero element $a$ in a group with zero $G_0$ and natural numbers $m$ and $n$ such that $n \leq m$, the $(m - n)$-th power of the inverse of $a$ equals the product of the inverse of $a^m$ and $a^n$, i.e., $(a^{-1})^{m - n} = (a^m)^{-1} \cdot a^n$.
inv_pow_sub_of_lt theorem
(a : G₀) (h : n < m) : a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
Full source 
lemma inv_pow_sub_of_lt (a : G₀) (h : n < m) : a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n := by
  rw [pow_sub_of_lt a⁻¹ h, inv_pow, inv_pow, inv_inv]
Inverse Power Subtraction Law for $n < m$: $(a^{-1})^{m-n} = (a^m)^{-1} \cdot a^n$ in Groups with Zero
Informal description
For any element $a$ in a group with zero $G_0$ and natural numbers $n$ and $m$ such that $n < m$, the $(m - n)$-th power of the inverse of $a$ equals the product of the inverse of $a^m$ and $a^n$, i.e., $(a^{-1})^{m - n} = (a^m)^{-1} \cdot a^n$.
zpow_sub₀ theorem
(ha : a ≠ 0) (m n : ℤ) : a ^ (m - n) = a ^ m / a ^ n
Full source 
lemma zpow_sub₀ (ha : a ≠ 0) (m n : ℤ) : a ^ (m - n) = a ^ m / a ^ n := by
  rw [Int.sub_eq_add_neg, zpow_add₀ ha, zpow_neg, div_eq_mul_inv]
Exponent Subtraction Law for Groups with Zero: $a^{m-n} = a^m / a^n$
Informal description
For any nonzero element $a$ in a group with zero $G_0$ and any integers $m$ and $n$, the $(m - n)$-th power of $a$ equals the $m$-th power of $a$ divided by the $n$-th power of $a$, i.e., $a^{m - n} = a^m / a^n$.
zpow_natCast_sub_natCast₀ theorem
(ha : a ≠ 0) (m n : ℕ) : a ^ (m - n : ℤ) = a ^ m / a ^ n
Full source 
lemma zpow_natCast_sub_natCast₀ (ha : a ≠ 0) (m n : ℕ) : a ^ (m - n : ℤ) = a ^ m / a ^ n := by
  simpa using zpow_sub₀ ha m n
Integer Power Subtraction Law for Groups with Zero: $a^{m-n} = a^m / a^n$
Informal description
For any nonzero element $a$ in a group with zero $G_0$ and any natural numbers $m$ and $n$, the integer power $a^{m-n}$ equals $a^m$ divided by $a^n$, i.e., $a^{m-n} = a^m / a^n$.
zpow_natCast_sub_one₀ theorem
(ha : a ≠ 0) (n : ℕ) : a ^ (n - 1 : ℤ) = a ^ n / a
Full source 
lemma zpow_natCast_sub_one₀ (ha : a ≠ 0) (n : ℕ) : a ^ (n - 1 : ℤ) = a ^ n / a := by
  simpa using zpow_sub₀ ha n 1
Integer Power Reduction: $a^{n-1} = a^n / a$ for $a \neq 0$
Informal description
For any nonzero element $a$ in a group with zero $G_0$ and any natural number $n$, the $(n-1)$-th integer power of $a$ equals the $n$-th power of $a$ divided by $a$, i.e., $a^{(n-1)} = a^n / a$.
zpow_one_sub_natCast₀ theorem
(ha : a ≠ 0) (n : ℕ) : a ^ (1 - n : ℤ) = a / a ^ n
Full source 
lemma zpow_one_sub_natCast₀ (ha : a ≠ 0) (n : ℕ) : a ^ (1 - n : ℤ) = a / a ^ n := by
  simpa using zpow_sub₀ ha 1 n
Exponent Identity: $a^{1 - n} = a / a^n$ for $a \neq 0$
Informal description
For any nonzero element $a$ in a group with zero $G_0$ and any natural number $n$, the $(1 - n)$-th integer power of $a$ equals $a$ divided by the $n$-th power of $a$, i.e., $a^{1 - n} = a / a^n$.
zpow_ne_zero theorem
{a : G₀} : ∀ n : ℤ, a ≠ 0 → a ^ n ≠ 0
Full source 
lemma zpow_ne_zero {a : G₀} : ∀ n : ℤ, a ≠ 0 → a ^ n ≠ 0
  | (_ : ℕ) => by rw [zpow_natCast]; exact pow_ne_zero _
  | .negSucc n => fun ha ↦ by rw [zpow_negSucc]; exact inv_ne_zero (pow_ne_zero _ ha)
Nonzero Elements Have Nonzero Integer Powers in Groups with Zero
Informal description
For any element $a$ in a group with zero $G_0$ and any integer $n$, if $a \neq 0$, then the integer power $a^n \neq 0$.
zpow_eq_zero_iff theorem
{n : ℤ} (hn : n ≠ 0) : a ^ n = 0 ↔ a = 0
Full source 
lemma zpow_eq_zero_iff {n : ℤ} (hn : n ≠ 0) : a ^ n = 0 ↔ a = 0 :=
  ⟨eq_zero_of_zpow_eq_zero, fun ha => ha.symm ▸ zero_zpow _ hn⟩
Zero Power Criterion in Groups with Zero: $a^n = 0 \leftrightarrow a = 0$ for $n \neq 0$
Informal description
For any integer $n \neq 0$ and any element $a$ in a group with zero $G_0$, the $n$-th power of $a$ equals zero if and only if $a$ itself is zero, i.e., $a^n = 0 \leftrightarrow a = 0$.
zpow_ne_zero_iff theorem
{n : ℤ} (hn : n ≠ 0) : a ^ n ≠ 0 ↔ a ≠ 0
Full source 
lemma zpow_ne_zero_iff {n : ℤ} (hn : n ≠ 0) : a ^ n ≠ 0a ^ n ≠ 0 ↔ a ≠ 0 := (zpow_eq_zero_iff hn).ne
Nonzero Power Criterion in Groups with Zero: $a^n \neq 0 \leftrightarrow a \neq 0$ for $n \neq 0$
Informal description
For any integer $n \neq 0$ and any element $a$ in a group with zero, 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$.
zpow_neg_mul_zpow_self theorem
(n : ℤ) (ha : a ≠ 0) : a ^ (-n) * a ^ n = 1
Full source 
lemma zpow_neg_mul_zpow_self (n : ℤ) (ha : a ≠ 0) : a ^ (-n) * a ^ n = 1 := by
  rw [zpow_neg]; exact inv_mul_cancel₀ (zpow_ne_zero n ha)
Inverse and Positive Power Product Identity: $a^{-n} \cdot a^n = 1$ for $a \neq 0$
Informal description
For any nonzero element $a$ in a group with zero $G_0$ and any integer $n$, the product of $a^{-n}$ and $a^n$ equals the multiplicative identity, i.e., $a^{-n} \cdot a^n = 1$.
Ring.inverse_eq_inv theorem
(a : G₀) : Ring.inverse a = a⁻¹
Full source 
theorem Ring.inverse_eq_inv (a : G₀) : Ring.inverse a = a⁻¹ := by
  obtain rfl | ha := eq_or_ne a 0
  · simp
  · exact Ring.inverse_unit (Units.mk0 a ha)
Global Inverse Equals Multiplicative Inverse in Groups with Zero
Informal description
For any element $a$ in a group with zero $G_0$, the globally defined inverse function satisfies $\text{inverse}(a) = a^{-1}$.
Ring.inverse_eq_inv' theorem
: (Ring.inverse : G₀ → G₀) = Inv.inv
Full source 
@[simp]
theorem Ring.inverse_eq_inv' : (Ring.inverse : G₀ → G₀) = Inv.inv :=
  funext Ring.inverse_eq_inv
Global Inverse Equals Multiplicative Inverse in Groups with Zero (Function Equality)
Informal description
The globally defined inverse function `Ring.inverse` on a group with zero $G_0$ coincides with the multiplicative inverse function $\text{Inv.inv}$, i.e., $\text{Ring.inverse} = \text{Inv.inv}$ as functions from $G_0$ to $G_0$.
div_mul_cancel_left₀ theorem
(ha : a ≠ 0) (b : G₀) : a / (a * b) = b⁻¹
Full source 
lemma div_mul_cancel_left₀ (ha : a ≠ 0) (b : G₀) : a / (a * b) = b⁻¹ :=
  ha.isUnit.div_mul_cancel_left _
Left Cancellation Property for Division in Commutative Groups with Zero: $a / (a \cdot b) = b^{-1}$ for $a \neq 0$
Informal description
For any nonzero element $a$ in a commutative group with zero $G_0$ and any element $b \in G_0$, the following holds: \[ a / (a \cdot b) = b^{-1}. \]
mul_div_cancel_left_of_imp theorem
(h : a = 0 → b = 0) : a * b / a = b
Full source 
lemma mul_div_cancel_left_of_imp (h : a = 0 → b = 0) : a * b / a = b := by
  rw [mul_comm, mul_div_cancel_of_imp h]
Left Cancellation Property for Multiplication and Division in Groups with Zero under Implication Condition
Informal description
For any elements $a$ and $b$ in a group with zero, if $a = 0$ implies $b = 0$, then $(a \cdot b) / a = b$.
mul_div_cancel_of_imp' theorem
(h : b = 0 → a = 0) : b * (a / b) = a
Full source 
lemma mul_div_cancel_of_imp' (h : b = 0 → a = 0) : b * (a / b) = a := by
  rw [mul_comm, div_mul_cancel_of_imp h]
Conditional Left Cancellation Property for Division in Groups with Zero: $b \cdot (a / b) = a$ when $b = 0 \Rightarrow a = 0$
Informal description
For any elements $a$ and $b$ in a group with zero $G_0$, if $b = 0$ implies $a = 0$, then $b \cdot (a / b) = a$.
mul_div_cancel₀ theorem
(a : G₀) (hb : b ≠ 0) : b * (a / b) = a
Full source 
lemma mul_div_cancel₀ (a : G₀) (hb : b ≠ 0) : b * (a / b) = a :=
  hb.isUnit.mul_div_cancel _
Cancellation Property for Division in Commutative Groups with Zero: $b \cdot (a / b) = a$ when $b \neq 0$
Informal description
For any elements $a$ and $b$ in a commutative group with zero $G_0$, if $b \neq 0$, then $b \cdot (a / b) = a$.
mul_div_mul_left theorem
(a b : G₀) (hc : c ≠ 0) : c * a / (c * b) = a / b
Full source 
lemma mul_div_mul_left (a b : G₀) (hc : c ≠ 0) : c * a / (c * b) = a / b :=
  hc.isUnit.mul_div_mul_left _ _
Left Cancellation Property for Nonzero Elements: $\frac{c \cdot a}{c \cdot b} = \frac{a}{b}$ when $c \neq 0$
Informal description
For any elements $a, b, c$ in a commutative group with zero $G_0$, if $c \neq 0$, then the following equality holds: \[ \frac{c \cdot a}{c \cdot b} = \frac{a}{b}. \]
mul_eq_mul_of_div_eq_div theorem
(a c : G₀) (hb : b ≠ 0) (hd : d ≠ 0) (h : a / b = c / d) : a * d = c * b
Full source 
lemma mul_eq_mul_of_div_eq_div (a c : G₀) (hb : b ≠ 0) (hd : d ≠ 0)
    (h : a / b = c / d) : a * d = c * b := by
  rw [← mul_one a, ← div_self hb, ← mul_comm_div, h, div_mul_eq_mul_div, div_mul_cancel₀ _ hd]
Cross-Multiplication Equality from Fraction Equality: $\frac{a}{b} = \frac{c}{d} \implies a \cdot d = c \cdot b$
Informal description
For any elements $a, c$ in a commutative group with zero $G_0$ and any nonzero elements $b, d$ (i.e., $b \neq 0$ and $d \neq 0$), if $\frac{a}{b} = \frac{c}{d}$, then $a \cdot d = c \cdot b$.
div_eq_div_iff theorem
(hb : b ≠ 0) (hd : d ≠ 0) : a / b = c / d ↔ a * d = c * b
Full source 
@[field_simps] lemma div_eq_div_iff (hb : b ≠ 0) (hd : d ≠ 0) : a / b = c / d ↔ a * d = c * b :=
  hb.isUnit.div_eq_div_iff hd.isUnit
Fraction Equality Criterion via Cross-Multiplication: $\frac{a}{b} = \frac{c}{d} \leftrightarrow a \cdot d = c \cdot b$
Informal description
For any elements $a, c$ in a commutative group with zero $G_0$ and any nonzero elements $b, d$ (i.e., $b \neq 0$ and $d \neq 0$), the equality of fractions $\frac{a}{b} = \frac{c}{d}$ holds if and only if the cross-multiplication equality $a \cdot d = c \cdot b$ holds.
div_eq_div_iff_div_eq_div' theorem
(hb : b ≠ 0) (hc : c ≠ 0) : a / b = c / d ↔ a / c = b / d
Full source 
/-- The `CommGroupWithZero` version of `div_eq_div_iff_div_eq_div`. -/
lemma div_eq_div_iff_div_eq_div' (hb : b ≠ 0) (hc : c ≠ 0) : a / b = c / d ↔ a / c = b / d := by
  conv_lhs => rw [← mul_left_inj' hb, div_mul_cancel₀ _ hb]
  conv_rhs => rw [← mul_left_inj' hc, div_mul_cancel₀ _ hc]
  rw [mul_comm _ c, div_mul_eq_mul_div, mul_div_assoc]
Fraction Equality Criterion via Reciprocal Fractions: $\frac{a}{b} = \frac{c}{d} \leftrightarrow \frac{a}{c} = \frac{b}{d}$ for $b, c \neq 0$
Informal description
For any elements $a, c, d$ in a commutative group with zero $G_0$ and any nonzero elements $b, c$ (i.e., $b \neq 0$ and $c \neq 0$), the equality of fractions $\frac{a}{b} = \frac{c}{d}$ holds if and only if the equality $\frac{a}{c} = \frac{b}{d}$ holds.
div_div_cancel₀ theorem
(ha : a ≠ 0) : a / (a / b) = b
Full source 
@[simp] lemma div_div_cancel₀ (ha : a ≠ 0) : a / (a / b) = b := ha.isUnit.div_div_cancel
Double Division Cancellation for Nonzero Elements: $a/(a/b) = b$
Informal description
For any nonzero element $a$ in a commutative group with zero and any element $b$, the expression $a / (a / b)$ simplifies to $b$.
div_div_cancel_left' theorem
(ha : a ≠ 0) : a / b / a = b⁻¹
Full source 
lemma div_div_cancel_left' (ha : a ≠ 0) : a / b / a = b⁻¹ := ha.isUnit.div_div_cancel_left
Double Division Cancellation for Nonzero Elements: $(a / b) / a = b^{-1}$
Informal description
For any nonzero element $a$ in a commutative group with zero $G₀$, and for any element $b \in G₀$, the following equality holds: $(a / b) / a = b^{-1}$.
div_helper theorem
(b : G₀) (h : a ≠ 0) : 1 / (a * b) * a = 1 / b
Full source 
lemma div_helper (b : G₀) (h : a ≠ 0) : 1 / (a * b) * a = 1 / b := by
  rw [div_mul_eq_mul_div, one_mul, div_mul_cancel_left₀ h, one_div]
Fraction Simplification Identity: $\frac{1}{a \cdot b} \cdot a = \frac{1}{b}$ for $a \neq 0$
Informal description
For any element $b$ in a commutative group with zero $G_0$ and any nonzero element $a \in G_0$, the following equality holds: \[ \frac{1}{a \cdot b} \cdot a = \frac{1}{b}. \]
div_div_div_cancel_left' theorem
(a b : G₀) (hc : c ≠ 0) : c / a / (c / b) = b / a
Full source 
lemma div_div_div_cancel_left' (a b : G₀) (hc : c ≠ 0) : c / a / (c / b) = b / a := by
  rw [div_div_div_eq, mul_comm, mul_div_mul_right _ _ hc]
Fraction Cancellation Identity: $\frac{c/a}{c/b} = \frac{b}{a}$ for $c \neq 0$
Informal description
For any elements $a, b, c$ in a commutative group with zero $G_0$, if $c \neq 0$, then the following equality holds: \[ \frac{c/a}{c/b} = \frac{b}{a}. \]
div_mul_div_cancel₀' theorem
(ha : a ≠ 0) (b c : G₀) : a / b * (c / a) = c / b
Full source 
@[simp] lemma div_mul_div_cancel₀' (ha : a ≠ 0) (b c : G₀) : a / b * (c / a) = c / b := by
  rw [mul_comm, div_mul_div_cancel₀ ha]
Fraction Cancellation Identity: $(a/b) \cdot (c/a) = c/b$ for $a \neq 0$
Informal description
For any elements $a, b, c$ in a group with zero $G_0$, if $a \neq 0$, then $(a / b) \cdot (c / a) = c / b$.
groupWithZeroOfIsUnitOrEqZero definition
[hM : MonoidWithZero M] (h : ∀ a : M, IsUnit a ∨ a = 0) : GroupWithZero M
Full source 
/-- Constructs a `GroupWithZero` structure on a `MonoidWithZero`
  consisting only of units and 0. -/
noncomputable def groupWithZeroOfIsUnitOrEqZero [hM : MonoidWithZero M]
    (h : ∀ a : M, IsUnitIsUnit a ∨ a = 0) : GroupWithZero M :=
  { hM with
    inv := fun a => if h0 : a = 0 then 0 else ↑((h a).resolve_right h0).unit⁻¹,
    inv_zero := dif_pos rfl,
    mul_inv_cancel := fun a h0 => by
      change (a * if h0 : a = 0 then 0 else ↑((h a).resolve_right h0).unit⁻¹) = 1
      rw [dif_neg h0, Units.mul_inv_eq_iff_eq_mul, one_mul, IsUnit.unit_spec],
    exists_pair_ne := Nontrivial.exists_pair_ne }
Group with zero structure on a monoid with zero where all non-zero elements are units
Informal description
Given a monoid with zero `M` where every element is either a unit or zero, this definition constructs a group with zero structure on `M`. The inverse function is defined as follows: - For `a = 0`, the inverse is `0`. - For `a ≠ 0`, the inverse is the inverse of `a` in the group of units of `M`.
commGroupWithZeroOfIsUnitOrEqZero definition
[hM : CommMonoidWithZero M] (h : ∀ a : M, IsUnit a ∨ a = 0) : CommGroupWithZero M
Full source 
/-- Constructs a `CommGroupWithZero` structure on a `CommMonoidWithZero`
  consisting only of units and 0. -/
noncomputable def commGroupWithZeroOfIsUnitOrEqZero [hM : CommMonoidWithZero M]
    (h : ∀ a : M, IsUnitIsUnit a ∨ a = 0) : CommGroupWithZero M :=
  { groupWithZeroOfIsUnitOrEqZero h, hM with }
Commutative group with zero structure on a monoid with zero where all non-zero elements are units
Informal description
Given a commutative monoid with zero `M` where every element is either a unit or zero, this definition constructs a commutative group with zero structure on `M`. The inverse function is defined as follows: - For `a = 0`, the inverse is `0`. - For `a ≠ 0`, the inverse is the inverse of `a` in the group of units of `M`.