lift_aeval — Mathlib

English

A compatibility lemma for lifting congruences along pb.lift, ensuring that lifting respects equality relations between pb and pb_1 under a homomorphism.

Русский

Лемма согласованности для переносов вдоль pb.lift, гарантирующая сохранение равенств между pb и pb_1 под однородным отображением.

LaTeX

$$pb.lift pb' y hy ≈ pb._? (конгруэнтность)$$

Lean4

@[simp]
theorem lift_aeval (pb : PowerBasis A S) (y : S') (hy : aeval y (minpoly A pb.gen) = 0) (f : A[X]) :
    pb.lift y hy (aeval pb.gen f) = aeval y f :=
  pb.constr_pow_aeval hy f

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