equivAdjoinSimple_aeval — Mathlib

English

There is a natural algebra isomorphism between the adjoined power basis and L, given by the equivalence pb.equivAdjoinSimple.

Русский

Существует естественный алгебраический изоморфизм между адъюнктом по базису мощности и самой L, задаваемый pb.equivAdjoinSimple.

LaTeX

$$PowerBasis.equivAdjoinSimple pb : K⟮pb.gen⟯ ≃ₐ[K] L$$

Lean4

@[simp]
theorem equivAdjoinSimple_aeval (pb : PowerBasis K L) (f : K[X]) :
    pb.equivAdjoinSimple (aeval (AdjoinSimple.gen K pb.gen) f) = aeval pb.gen f :=
  equivOfMinpoly_aeval _ pb _ f

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