English
Let pb and pb' be power bases of A-algebras S and S' respectively, and suppose pb.gen is a root of the minimal polynomial of pb'.gen and pb'.gen is a root of the minimal polynomial of pb.gen. Then for every polynomial f in A[X], the algebra isomorphism pb.equivOfRoot pb' h1 h2 sends aeval pb.gen f to aeval pb'.gen f.
Русский
Пусть pb и pb' — базисы по степени над A для алгебр S и S' соответственно. Пусть pb.gen является корнем минимального полинома pb'.gen и pb'.gen является корнем минимального полинома pb.gen. Тогда для каждого многочлена f ∈ A[X] изоморфизм pb.equivOfRoot pb' h1 h2 отправляет aeval pb.gen f в aeval pb'.gen f.
LaTeX
$$$\\forall pb pb' (h_1 : aeval pb.gen (minpoly A pb'.gen) = 0) (h_2 : aeval pb'.gen (minpoly A pb.gen) = 0) (f : A[X]),\\ pb.equivOfRoot pb' h_1 h_2 (aeval pb.gen f) = aeval pb'.gen f.$$$
Lean4
@[simp]
theorem equivOfRoot_aeval (pb : PowerBasis A S) (pb' : PowerBasis A S') (h₁ : aeval pb.gen (minpoly A pb'.gen) = 0)
(h₂ : aeval pb'.gen (minpoly A pb.gen) = 0) (f : A[X]) :
pb.equivOfRoot pb' h₁ h₂ (aeval pb.gen f) = aeval pb'.gen f :=
pb.lift_aeval _ h₂ _
