transfer_galois — Mathlib

English

If f is an algebra equivalence between E and E' over F, then E is Galois over F if and only if E' is Galois over F.

Русский

Если есть алгебраическое эквивалентное отображение между E и E' над F, то Галуа-расширение сохраняется.

LaTeX

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

Lean4

theorem transfer_galois (f : E ≃ₐ[F] E') : IsGalois F E ↔ IsGalois F E' :=
  ⟨fun _ => IsGalois.of_algEquiv f, fun _ => IsGalois.of_algEquiv f.symm⟩

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