div_mem — Mathlib

English

Let S be an intermediate field of L over K. Then S is closed under division: if x,y ∈ S with y ≠ 0, then x/y ∈ S.

Русский

Пусть S — промежутое поле L над K. Тогда S замкнуто относительно деления: если x,y ∈ S и y ≠ 0, то x/y ∈ S.

LaTeX

$$$\forall x,y \in S:\ x / y \in S$$$

Lean4

/-- An intermediate field is closed under division. -/
protected theorem div_mem {x y : L} : x ∈ S → y ∈ S → x / y ∈ S :=
  div_mem

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