inv_mem — Mathlib

English

Let S be an intermediate field of L over K. Then S is closed under multiplicative inverses: if x ∈ S, then x⁻¹ ∈ S.

Русский

Пусть S — промежутое поле L над K. Тогда S замкнуто относительно обратного элемента: если x ∈ S, то x⁻¹ ∈ S.

LaTeX

$$$\forall x \in S:\ x^{-1} \in S$$$

Lean4

/-- An intermediate field is closed under inverses. -/
protected theorem inv_mem {x : L} : x ∈ S → x⁻¹ ∈ S :=
  inv_mem

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