isGalois_iff_isGalois_top — Mathlib

English

For any F, E, the statement IsGalois F (⊤ : IntermediateField F E) ↔ IsGalois F E holds, reflecting the top equivalence.

Русский

Для любых F, E утверждение IsGalois F (⊤) ↔ IsGalois F E отражает верхнюю эквивалентность.

LaTeX

$$IsGalois F (⊤ : IntermediateField F E) ↔ IsGalois F E$$

Lean4

theorem isGalois_iff_isGalois_top : IsGalois F (⊤ : IntermediateField F E) ↔ IsGalois F E :=
  (IntermediateField.topEquiv : (⊤ : IntermediateField F E) ≃ₐ[F] E).transfer_galois

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