inv_mem — Mathlib

English

Let K be a division ring and s ⊆ K be a subfield. Then for every x ∈ s, the inverse x^{-1} is also in s.

Русский

Пусть K — деление кольцо, и s ⊆ K будет подполем. Тогда для любого x ∈ s обратное x^{-1} также принадлежит s.

LaTeX

$$$x \in s \Rightarrow x^{-1} \in s$$$

Lean4

/-- A subfield is closed under inverses. -/
protected theorem inv_mem {x : K} : x ∈ s → x⁻¹ ∈ s :=
  inv_mem

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