adjoin_simple_le_iff — Mathlib

English

For IsGalois k K, and any x ∈ K, adjoin k {x} ≤ L iff x ∈ L.toIntermediateField.

Русский

Пусть k ⊆ K/Galois; тогда adjoin_k({x}) ≤ L эквивалентно x ∈ L.toIntermediateField.

LaTeX

$$$ adjoin_k(\{x\}) \le L \iff x \in L.toIntermediateField. $$$

Lean4

theorem adjoin_simple_le_iff [IsGalois k K] {x : K} {L : FiniteGaloisIntermediateField k K} :
    adjoin k { x } ≤ L ↔ x ∈ L.toIntermediateField := by
  simp only [le_iff, adjoin_val, IntermediateField.normalClosure_le_iff_of_normal, IntermediateField.adjoin_le_iff,
    Set.singleton_subset_iff, SetLike.mem_coe]

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