of_algEquiv — Mathlib

English

For any F-algebra isomorphism f: E ≃ₐ[F] E', Normal F E holds iff Normal F E' holds.

Русский

Для любого тождественного по F-алгебре отображения f: E ≃ₐ[F] E' имеем: Normal F E эквивалентно Normal F E'.

LaTeX

$$$\mathrm{Normal} F E \iff \mathrm{Normal} F E'$ через $f$$$

Lean4

theorem of_algEquiv [h : Normal F E] (f : E ≃ₐ[F] E') : Normal F E' :=
  by
  rw [normal_iff] at h ⊢
  intro x; specialize h (f.symm x)
  rw [← f.apply_symm_apply x, minpoly.algEquiv_eq, ← f.toAlgHom.comp_algebraMap]
  exact ⟨h.1.map f, splits_comp_of_splits _ _ h.2⟩

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