ext — Mathlib

English

Two subfields are equal if they have the same elements; equality is determined by set membership.

Русский

Два подполе равны, если у них совпадают элементы; равенство задаётся по множеству элементов.

LaTeX

$$@ext {S T : Subfield K} (h : ∀ x, x ∈ S ↔ x ∈ T) : S = T$$

Lean4

/-- Two subfields are equal if they have the same elements. -/
@[ext]
theorem ext {S T : Subfield K} (h : ∀ x, x ∈ S ↔ x ∈ T) : S = T :=
  SetLike.ext h

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