le_iff — Mathlib

English

For any two finite Galois intermediate fields L1, L2, the order relation in the FGIF lattice agrees with the order of their underlying intermediate fields.

Русский

Порядок в решётке FGIF совпадает с порядком соответствующих подполей над промежуточным полем.

LaTeX

$$$ L_1 \le L_2 \iff L_1.toIntermediateField \le L_2.toIntermediateField. $$$

Lean4

@[simp]
theorem le_iff (L₁ L₂ : FiniteGaloisIntermediateField k K) :
    L₁ ≤ L₂ ↔ L₁.toIntermediateField ≤ L₂.toIntermediateField :=
  Iff.rfl

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