coeff_map — Mathlib

English

Taking the n-th coefficient commutes with applying a ring homomorphism to the entire power series.

Русский

Взятие n-ого коэффициента и применение кольцевого гомоморфизма к степенному ряду ведут к одинаковым результатам: coeff_n(map f φ) = f(coeff_n φ).

LaTeX

$$$\operatorname{coeff}_n(\mathrm{map} f\, \phi) = f\big(\operatorname{coeff}_n \phi\big)$$$

Lean4

@[simp]
theorem coeff_map (n : ℕ) (φ : R⟦X⟧) : coeff n (map f φ) = f (coeff n φ) :=
  rfl

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