lift_mk — Mathlib

English

Lifting a polynomial from R[X] to the quotient by f yields evaluation at the corresponding coefficient ring element.

Русский

Поднятие полинома из R[X] в фактор-кольцо по f даёт эквивалентное вычисление коэффициентов полинома g через i и a.

LaTeX

$$$\mathrm{lift}(i, a, h)(\mathrm{mk}(f,g)) = g\!\_{{\mathrm{eval}}_2 i a}$$$

Lean4

@[simp]
theorem lift_mk (g : R[X]) : lift i a h (mk f g) = g.eval₂ i a :=
  Ideal.Quotient.lift_mk _ _ _

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