of_algEquiv — Mathlib

English

If f is IsSplittingField over F and f is transported along an algebra equivalence f: F ≃ₐ[K] L, then p remains IsSplittingField over K L.

Русский

Если многочлен f является IsSplittingField над F и переносится через алгебраическое эквивалентное отображение, то свойство сохраняется.

LaTeX

$$of_algEquiv$$

Lean4

theorem of_algEquiv [Algebra K F] (p : K[X]) (f : F ≃ₐ[K] L) [IsSplittingField K F p] : IsSplittingField K L p :=
  by
  constructor
  · rw [← f.toAlgHom.comp_algebraMap]
    exact splits_comp_of_splits _ _ (splits F p)
  · rw [← (AlgHom.range_eq_top f.toAlgHom).mpr f.surjective, adjoin_rootSet_eq_range (splits F p), adjoin_rootSet F p]

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