constantCoeff_map — Mathlib

English

The constant term commutes with coefficient maps: constantCoeff (map f φ) = f (constantCoeff φ).

Русский

Константный коэффициент ведет себя совместно с отображениями коэффициентов: constantCoeff (map f φ) = f (constantCoeff φ).

LaTeX

$$$\\operatorname{constantCoeff}(\\mathrm{map} f \\; \\phi) = f\\big( \\operatorname{constantCoeff}(\\phi) \\big)$$$

Lean4

@[simp]
theorem constantCoeff_map (φ : MvPowerSeries σ R) : constantCoeff (map f φ) = f (constantCoeff φ) :=
  rfl

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