inv_mem — Mathlib

English

If a ∈ RingPreordering F for a field F, then a^{-1} ∈ RingPreordering F.

Русский

Если элемент a ∈ RingPreordering F для поля F, то a^{-1} ∈ RingPreordering F.

LaTeX

$$If $a \\in P$ for Field $F$, then $a^{-1} \\in P$$$

Lean4

@[aesop unsafe 90% apply (rule_sets := [SetLike])]
theorem inv_mem {F : Type*} [Field F] {P : RingPreordering F} {a : F} (ha : a ∈ P) : a⁻¹ ∈ P :=
  by
  have mem : a * (a⁻¹ * a⁻¹) ∈ P := by aesop
  field_simp at mem
  simp_all

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