equivOfMinpoly_map — Mathlib

English

For pb : PowerBasis A S and e : S ≃ₐ[A] S', with h : minpoly A pb.gen = minpoly A (pb.map e).gen, the isomorphism pb.equivOfMinpoly pb.map e h equals e.

Русский

Пусть pb : PowerBasis A S и e : S ≃ₐ[A] S', и h : минполином(pb.gen) = минполином((pb.map e).gen). Тогда pb.equivOfMinpoly pb.map e h = e.

LaTeX

$$$ pb.equivOfMinpoly (pb.map e) h = e $$$

Lean4

@[simp]
theorem equivOfMinpoly_map (pb : PowerBasis A S) (e : S ≃ₐ[A] S') (h : minpoly A pb.gen = minpoly A (pb.map e).gen) :
    pb.equivOfMinpoly (pb.map e) h = e :=
  pb.equivOfRoot_map _ _ _

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