inv_eq_self_iff — Mathlib

English

In the unit group of an integral domain, u^{-1} = u iff u = 1 or u = −1.

Русский

В группе единиц интегрального домена, u^{-1} = u тогда и только тогда, когда u = 1 или u = −1.

LaTeX

$$$ u^{-1} = u \\iff u = 1 \\lor u = -1 $$$

Lean4

/-- In the unit group of an integral domain, a unit is its own inverse iff the unit is one or
  one's additive inverse. -/
theorem inv_eq_self_iff [Ring R] [NoZeroDivisors R] (u : Rˣ) : u⁻¹ = u ↔ u = 1 ∨ u = -1 :=
  by
  rw [inv_eq_iff_mul_eq_one]
  simp only [Units.ext_iff]
  push_cast
  exact mul_self_eq_one_iff

Похожие утверждения