isGalois_iff_isGalois_bot — Mathlib

English

For any F-algebra isomorphism f: E ≃ₐ[F] E', E is Galois over F if and only if E' is Galois over F.

Русский

Для любого изоморфизма f: E ≃ₐ[F] E' расширение E/ F Галуа тогда и только тогда, когда E'/F Галуа.

LaTeX

$$IsGalois F E ↔ IsGalois F E'$$

Lean4

theorem isGalois_iff_isGalois_bot : IsGalois (⊥ : IntermediateField F E) E ↔ IsGalois F E :=
  by
  constructor
  · intro h
    exact IsGalois.tower_top_of_isGalois (⊥ : IntermediateField F E) F E
  · intro h; infer_instance

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