coeff_restriction' — Mathlib

English

The same statement as coeff_restriction holds after projecting to the underlying ring: the nth coefficient of restriction(p) equals p_n.

Русский

То же самое для проекции на осн.norm: коэффициент при n многочлена restriction(p) равен p_n.

LaTeX

$$$(\operatorname{coeff}(\operatorname{restriction} p) n).1 = \operatorname{coeff} p n$$$

Lean4

theorem coeff_restriction' {p : R[X]} {n : ℕ} : (coeff (restriction p) n).1 = coeff p n := by simp

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