English
Two power bases pb and pb' with h : minpoly A pb.gen = minpoly A pb'.gen determine an algebra isomorphism between S and S', denoted pb.equivOfMinpoly pb' h, i.e. pb.equivOfMinpoly pb' h : S ≃ₐ[A] S'.
Русский
Даны power-базисы pb и pb' и тождество минимальных полиномов pb.gen и pb'.gen. Тогда существует A-алгебра-однородность pb.equivOfMinpoly pb' h: S ≃ₐ[A] S'.
LaTeX
$$$ pb.equivOfMinpoly pb' h : S \cong_A S' $$$
Lean4
/-- `pb.equivOfMinpoly pb' h` is an equivalence of algebras with the same power basis,
where "the same" means that they have identical minimal polynomials.
See also `PowerBasis.equivOfRoot` which takes the hypothesis that each generator is a root of the
other basis' minimal polynomial; `PowerBasis.equivOfRoot` is more general if `A` is not a field.
-/
@[simps! -isSimp apply]
noncomputable def equivOfMinpoly (pb : PowerBasis A S) (pb' : PowerBasis A S')
(h : minpoly A pb.gen = minpoly A pb'.gen) : S ≃ₐ[A] S' :=
pb.equivOfRoot pb' (h ▸ minpoly.aeval _ _) (h.symm ▸ minpoly.aeval _ _)
