unitsInv_mem — Mathlib

English

If a unit a ∈ R is in RingPreordering P, then its inverse a^{-1} ∈ P.

Русский

Если элемент-единица a ∈ R принадлежит RingPreordering P, то и его обратный a^{-1} принадлежит P.

LaTeX

$$If $a \\in P$ and $a \\in R^{\\times}$, then $a^{-1} \\in P$$$

Lean4

@[aesop unsafe 90% apply (rule_sets := [SetLike])]
theorem unitsInv_mem {a : Rˣ} (ha : ↑a ∈ P) : ↑a⁻¹ ∈ P :=
  by
  have : (a * (a⁻¹ * a⁻¹) : R) ∈ P := by aesop (config := { enableSimp := false })
  simp_all

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