isOpen_and_normal_iff_finite_and_isGalois

English

For L in a Galois extension, L.fixingSubgroup.carrier is open and normal iff L is finite-dimensional over k and L is Galois over k.

Русский

Для L в Галуа-расширении L.fixingSubgroup.carrier открыто и нормально тогда и только тогда, когда L конечномерно над k и L — Галуа над k.

LaTeX

$$$ IsOpen L.fixingSubgroup.carrier \wedge L.fixingSubgroup.Normal \\iff FiniteDimensional k L \wedge IsGalois k L $$$

Lean4

theorem isOpen_and_normal_iff_finite_and_isGalois (L : IntermediateField k K) [IsGalois k K] :
    IsOpen L.fixingSubgroup.carrier ∧ L.fixingSubgroup.Normal ↔ FiniteDimensional k L ∧ IsGalois k L := by
  rw [isOpen_iff_finite, normal_iff_isGalois]

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