equivOfMinpoly_aeval — Mathlib

English

If h : minpoly A pb.gen = minpoly A pb'.gen, then for all f in A[X], pb.equivOfMinpoly pb' h (aeval pb.gen f) = aeval pb'.gen f.

Русский

Пусть minpoly A pb.gen = minpoly A pb'.gen. Тогда для всех f ∈ A[X] выполняется pb.equivOfMinpoly pb' h (aeval pb.gen f) = aeval pb'.gen f.

LaTeX

$$$ pb.equivOfMinpoly pb' h (aeval pb.gen f) = aeval pb'.gen f $$$

Lean4

@[simp]
theorem equivOfMinpoly_aeval (pb : PowerBasis A S) (pb' : PowerBasis A S') (h : minpoly A pb.gen = minpoly A pb'.gen)
    (f : A[X]) : pb.equivOfMinpoly pb' h (aeval pb.gen f) = aeval pb'.gen f :=
  pb.equivOfRoot_aeval pb' _ _ _

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