isUnit_ringInverse — Mathlib

English

IsUnit(a) implies IsUnit(Ring.inverse a) and conversely.

Русский

IsUnit(a) тогда и только тогда IsUnit(Ring.inverse a).

LaTeX

$$$\text{IsUnit}(\operatorname{Ring.inverse}(a)) \iff \text{IsUnit}(a)$$$

Lean4

@[simp]
theorem isUnit_ringInverse {a : M₀} : IsUnit (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⟩

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