coeff_C — Mathlib

English

Repeatedly, coefficient after mapRange equals applying g to the coefficient: coeff m (mapRange g hg φ) = g (coeff m φ).

Русский

Снова коэффициент после mapRange равен применению g к коэффициенту: coeff m (mapRange g hg φ) = g (coeff m φ).

LaTeX

$$$\mathrm{coeff}\;m (\mathrm{mapRange}\ g\ hg\ \varphi) = g(\mathrm{coeff}\;m\ \varphi)$$$

Lean4

@[simp]
theorem coeff_C [DecidableEq σ] (m) (a) : coeff m (C a : MvPolynomial σ R) = if 0 = m then a else 0 :=
  Finsupp.single_apply

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