Mathlib.Algebra.GroupWithZero.Invertible

Invertible.ne_zero theorem

[MulZeroOneClass α] (a : α) [Nontrivial α] [Invertible a] : a ≠ 0

Full source

theorem Invertible.ne_zero [MulZeroOneClass α] (a : α) [Nontrivial α] [Invertible a] : a ≠ 0 :=
  fun ha =>
  zero_ne_one <|
    calc
      0 = ⅟ a * a := by simp [ha]
      _ = 1 := invOf_mul_self

Invertible Elements are Nonzero in Nontrivial Monoids with Zero

Informal description

For any element $a$ in a nontrivial monoid with zero $\alpha$, if $a$ is invertible, then $a$ is not equal to zero, i.e., $a \neq 0$.

Invertible.toNeZero instance

[MulZeroOneClass α] [Nontrivial α] (a : α) [Invertible a] : NeZero a

Full source

instance (priority := 100) Invertible.toNeZero [MulZeroOneClass α] [Nontrivial α] (a : α)
    [Invertible a] : NeZero a :=
  ⟨Invertible.ne_zero a⟩

Invertible Elements are Nonzero in Nontrivial Monoids with Zero

Informal description

For any element $a$ in a nontrivial monoid with zero $\alpha$, if $a$ is invertible, then $a$ is a nonzero element.

Ring.inverse_invertible theorem

(x : α) [Invertible x] : Ring.inverse x = ⅟ x

Full source

/-- A variant of `Ring.inverse_unit`. -/
@[simp]
theorem Ring.inverse_invertible (x : α) [Invertible x] : Ring.inverse x = ⅟ x :=
  Ring.inverse_unit (unitOfInvertible _)

Ring Inverse of Invertible Element Equals Multiplicative Inverse

Informal description

For any element $x$ in a monoid $\alpha$ that is invertible, the ring inverse of $x$ is equal to its multiplicative inverse, i.e., $\text{Ring.inverse}(x) = ⅟x$.

invertibleOfNonzero definition

{a : α} (h : a ≠ 0) : Invertible a

Full source

/-- `a⁻¹` is an inverse of `a` if `a ≠ 0` -/
def invertibleOfNonzero {a : α} (h : a ≠ 0) : Invertible a :=
  ⟨a⁻¹, inv_mul_cancel₀ h, mul_inv_cancel₀ h⟩

Existence of inverse for nonzero elements in a group with zero

Informal description

For any nonzero element $a$ in a group with zero, there exists a two-sided multiplicative inverse of $a$.

invOf_eq_inv theorem

(a : α) [Invertible a] : ⅟ a = a⁻¹

Full source

@[simp]
theorem invOf_eq_inv (a : α) [Invertible a] : ⅟ a = a⁻¹ :=
  invOf_eq_right_inv (mul_inv_cancel₀ (Invertible.ne_zero a))

Invertible Element's Inverse Equals Multiplicative Inverse: $⅟a = a^{-1}$

Informal description

For any invertible element $a$ in a monoid $\alpha$, the inverse of $a$ (denoted $⅟a$) is equal to the multiplicative inverse $a^{-1}$.

inv_mul_cancel_of_invertible theorem

(a : α) [Invertible a] : a⁻¹ * a = 1

Full source

@[simp]
theorem inv_mul_cancel_of_invertible (a : α) [Invertible a] : a⁻¹ * a = 1 :=
  inv_mul_cancel₀ (Invertible.ne_zero a)

Inverse Cancellation: $a^{-1} \cdot a = 1$ for Invertible Elements

Informal description

For any invertible element $a$ in a monoid with zero, the product of the inverse $a^{-1}$ and $a$ equals the multiplicative identity $1$, i.e., $a^{-1} \cdot a = 1$.

mul_inv_cancel_of_invertible theorem

(a : α) [Invertible a] : a * a⁻¹ = 1

Full source

@[simp]
theorem mul_inv_cancel_of_invertible (a : α) [Invertible a] : a * a⁻¹ = 1 :=
  mul_inv_cancel₀ (Invertible.ne_zero a)

Invertible Element Cancellation: $a \cdot a^{-1} = 1$

Informal description

For any invertible element $a$ in a monoid with zero, the product of $a$ and its inverse $a^{-1}$ equals the multiplicative identity $1$, i.e., $a \cdot a^{-1} = 1$.

invertibleInv definition

{a : α} [Invertible a] : Invertible a⁻¹

Full source

/-- `a` is the inverse of `a⁻¹` -/
def invertibleInv {a : α} [Invertible a] : Invertible a⁻¹ :=
  ⟨a, by simp, by simp⟩

Invertibility of the inverse element

Informal description

For any invertible element $a$ in a monoid with zero, the inverse $a^{-1}$ is also invertible, with $a$ as its inverse.

div_mul_cancel_of_invertible theorem

(a b : α) [Invertible b] : a / b * b = a

Full source

@[simp]
theorem div_mul_cancel_of_invertible (a b : α) [Invertible b] : a / b * b = a :=
  div_mul_cancel₀ a (Invertible.ne_zero b)

Division-Multiplication Cancellation for Invertible Elements

Informal description

For any elements $a$ and $b$ in a group with zero $\alpha$, if $b$ is invertible, then $(a / b) \cdot b = a$.

mul_div_cancel_of_invertible theorem

(a b : α) [Invertible b] : a * b / b = a

Full source

@[simp]
theorem mul_div_cancel_of_invertible (a b : α) [Invertible b] : a * b / b = a :=
  mul_div_cancel_right₀ a (Invertible.ne_zero b)

Multiplication-Division Cancellation for Invertible Elements

Informal description

For any elements $a$ and $b$ in a group with zero $\alpha$, if $b$ is invertible, then $(a \cdot b) / b = a$.

div_self_of_invertible theorem

(a : α) [Invertible a] : a / a = 1

Full source

@[simp]
theorem div_self_of_invertible (a : α) [Invertible a] : a / a = 1 :=
  div_self (Invertible.ne_zero a)

Self-Division of Invertible Elements Yields One

Informal description

For any invertible element $a$ in a group with zero $\alpha$, the division of $a$ by itself equals the multiplicative identity, i.e., $a / a = 1$.

invertibleDiv definition

(a b : α) [Invertible a] [Invertible b] : Invertible (a / b)

Full source

/-- `b / a` is the inverse of `a / b` -/
def invertibleDiv (a b : α) [Invertible a] [Invertible b] : Invertible (a / b) :=
  ⟨b / a, by simp [← mul_div_assoc], by simp [← mul_div_assoc]⟩

Invertibility of Quotient of Invertible Elements

Informal description

For any elements $a$ and $b$ in a group with zero $\alpha$, if both $a$ and $b$ are invertible, then the quotient $a / b$ is also invertible, with its inverse given by $b / a$.

invOf_div theorem

(a b : α) [Invertible a] [Invertible b] [Invertible (a / b)] : ⅟ (a / b) = b / a

Full source

theorem invOf_div (a b : α) [Invertible a] [Invertible b] [Invertible (a / b)] :
    ⅟ (a / b) = b / a :=
  invOf_eq_right_inv (by simp [← mul_div_assoc])

Inverse of Quotient: $⅟(a / b) = b / a$ for Invertible Elements

Informal description

For any elements $a$ and $b$ in a group with zero $\alpha$, if $a$, $b$, and $a / b$ are invertible, then the inverse of $a / b$ is equal to $b / a$, i.e., $⅟(a / b) = b / a$.