Mathlib.Algebra.Ring.Invertible

invertibleNeg definition

[Mul R] [One R] [HasDistribNeg R] (a : R) [Invertible a] : Invertible (-a)

Full source

/-- `-⅟a` is the inverse of `-a` -/
def invertibleNeg [Mul R] [One R] [HasDistribNeg R] (a : R) [Invertible a] : Invertible (-a) :=
  ⟨-⅟ a, by simp, by simp⟩

Invertibility of negation

Informal description

For any element $a$ in a multiplicative monoid $R$ with a one element and distributive negation, if $a$ is invertible with inverse $⅟a$, then $-a$ is also invertible with inverse $-⅟a$.

invOf_neg theorem

[Monoid R] [HasDistribNeg R] (a : R) [Invertible a] [Invertible (-a)] : ⅟ (-a) = -⅟ a

Full source

@[simp]
theorem invOf_neg [Monoid R] [HasDistribNeg R] (a : R) [Invertible a] [Invertible (-a)] :
    ⅟ (-a) = -⅟ a :=
  invOf_eq_right_inv (by simp)

Inverse of Negation: $⅟(-a) = -⅟a$

Informal description

Let $R$ be a monoid with a distributive negation operation. For any invertible element $a \in R$ with inverse $⅟a$, the inverse of $-a$ is $-⅟a$, i.e., $⅟(-a) = -⅟a$.

one_sub_invOf_two theorem

[Ring R] [Invertible (2 : R)] : 1 - (⅟ 2 : R) = ⅟ 2

Full source

@[simp]
theorem one_sub_invOf_two [Ring R] [Invertible (2 : R)] : 1 - (⅟ 2 : R) = ⅟ 2 :=
  (isUnit_of_invertible (2 : R)).mul_right_inj.1 <| by
    rw [mul_sub, mul_invOf_self, mul_one, ← one_add_one_eq_two, add_sub_cancel_right]

Identity for Halves: $1 - ⅟2 = ⅟2$ in Rings with Invertible 2

Informal description

Let $R$ be a ring where $2$ is invertible. Then $1 - ⅟2 = ⅟2$.

invOf_two_add_invOf_two theorem

[NonAssocSemiring R] [Invertible (2 : R)] : (⅟ 2 : R) + (⅟ 2 : R) = 1

Full source

@[simp]
theorem invOf_two_add_invOf_two [NonAssocSemiring R] [Invertible (2 : R)] :
    (⅟ 2 : R) + (⅟ 2 : R) = 1 := by rw [← two_mul, mul_invOf_self]

Sum of Halves Equals One in Non-Associative Semiring: $⅟2 + ⅟2 = 1$

Informal description

Let $R$ be a non-associative semiring where the element $2$ is invertible. Then the sum of the inverse of $2$ with itself equals $1$, i.e., $⅟2 + ⅟2 = 1$.

pos_of_invertible_cast theorem

[NonAssocSemiring R] [Nontrivial R] (n : ℕ) [Invertible (n : R)] : 0 < n

Full source

theorem pos_of_invertible_cast [NonAssocSemiring R] [Nontrivial R] (n : ℕ) [Invertible (n : R)] :
    0 < n :=
  Nat.zero_lt_of_ne_zero fun h => Invertible.ne_zero (n : R) (h ▸ Nat.cast_zero)

Invertibility of Natural Number Cast Implies Positivity

Informal description

Let $R$ be a nontrivial non-associative semiring. For any natural number $n$, if the canonical image of $n$ in $R$ is invertible, then $n$ is positive, i.e., $0 < n$.

invOf_add_invOf theorem

[Semiring R] (a b : R) [Invertible a] [Invertible b] : ⅟ a + ⅟ b = ⅟ a * (a + b) * ⅟ b

Full source

theorem invOf_add_invOf [Semiring R] (a b : R) [Invertible a] [Invertible b] :
    ⅟a + ⅟b = ⅟a * (a + b) * ⅟b := by
  rw [mul_add, invOf_mul_self, add_mul, one_mul, mul_assoc, mul_invOf_self, mul_one, add_comm]

Sum of Inverses Formula: $⅟a + ⅟b = ⅟a \cdot (a + b) \cdot ⅟b$

Informal description

For any elements $a$ and $b$ in a semiring $R$ that are invertible, the sum of their inverses satisfies the identity: \[ ⅟a + ⅟b = ⅟a \cdot (a + b) \cdot ⅟b. \]

invOf_sub_invOf theorem

[Ring R] (a b : R) [Invertible a] [Invertible b] : ⅟ a - ⅟ b = ⅟ a * (b - a) * ⅟ b

Full source

/-- A version of `inv_sub_inv'` for `invOf`. -/
theorem invOf_sub_invOf [Ring R] (a b : R) [Invertible a] [Invertible b] :
    ⅟a - ⅟b = ⅟a * (b - a) * ⅟b := by
  rw [mul_sub, invOf_mul_self, sub_mul, one_mul, mul_assoc, mul_invOf_self, mul_one]

Difference of Inverses Formula: $⅟a - ⅟b = ⅟a \cdot (b - a) \cdot ⅟b$

Informal description

For any elements $a$ and $b$ in a ring $R$ that are invertible, the difference of their inverses satisfies the identity: \[ ⅟a - ⅟b = ⅟a \cdot (b - a) \cdot ⅟b. \]

Ring.inverse_add_inverse theorem

 [Semiring R] {a b : R} (h : IsUnit a ↔ IsUnit b) :
  Ring.inverse a + Ring.inverse b = Ring.inverse a * (a + b) * Ring.inverse b

Full source

/-- A version of `inv_add_inv'` for `Ring.inverse`. -/
theorem Ring.inverse_add_inverse [Semiring R] {a b : R} (h : IsUnitIsUnit a ↔ IsUnit b) :
    Ring.inverse a + Ring.inverse b = Ring.inverse a * (a + b) * Ring.inverse b := by
  by_cases ha : IsUnit a
  · have hb := h.mp ha
    obtain ⟨ia⟩ := ha.nonempty_invertible
    obtain ⟨ib⟩ := hb.nonempty_invertible
    simp_rw [inverse_invertible, invOf_add_invOf]
  · have hb := h.not.mp ha
    simp [inverse_non_unit, ha, hb]

Sum of Ring Inverses Formula: $\text{inv}(a) + \text{inv}(b) = \text{inv}(a) \cdot (a + b) \cdot \text{inv}(b)$

Informal description

For any elements $a$ and $b$ in a semiring $R$ such that $a$ is a unit if and only if $b$ is a unit, the sum of their ring inverses satisfies: \[ \text{Ring.inverse}(a) + \text{Ring.inverse}(b) = \text{Ring.inverse}(a) \cdot (a + b) \cdot \text{Ring.inverse}(b). \]

Ring.inverse_sub_inverse theorem

 [Ring R] {a b : R} (h : IsUnit a ↔ IsUnit b) :
  Ring.inverse a - Ring.inverse b = Ring.inverse a * (b - a) * Ring.inverse b

Full source

/-- A version of `inv_sub_inv'` for `Ring.inverse`. -/
theorem Ring.inverse_sub_inverse [Ring R] {a b : R} (h : IsUnitIsUnit a ↔ IsUnit b) :
    Ring.inverse a - Ring.inverse b = Ring.inverse a * (b - a) * Ring.inverse b := by
  by_cases ha : IsUnit a
  · have hb := h.mp ha
    obtain ⟨ia⟩ := ha.nonempty_invertible
    obtain ⟨ib⟩ := hb.nonempty_invertible
    simp_rw [inverse_invertible, invOf_sub_invOf]
  · have hb := h.not.mp ha
    simp [inverse_non_unit, ha, hb]

Difference of Ring Inverses Formula: $\text{Ring.inverse}(a) - \text{Ring.inverse}(b) = \text{Ring.inverse}(a) \cdot (b - a) \cdot \text{Ring.inverse}(b)$

Informal description

Let $R$ be a ring and let $a, b \in R$ be elements such that $a$ is a unit if and only if $b$ is a unit. Then the difference of their ring inverses satisfies: \[ \text{Ring.inverse}(a) - \text{Ring.inverse}(b) = \text{Ring.inverse}(a) \cdot (b - a) \cdot \text{Ring.inverse}(b). \]