rescale_zero_apply — Mathlib

English

Scaling by zero acts as the constant-coefficient map: rescale 0 is the composition of the constant coefficient map with the constant term embedding.

Русский

Масштабирование нуля действует как отображение константного коэффициента за счёт композиции с константный коэффициент.

LaTeX

$$$\operatorname{rescale}(0) = \mathrm{C} \circ \mathrm{constantCoeff}$$$

Lean4

theorem rescale_zero_apply (f : MvPowerSeries σ R) : rescale 0 f = C (constantCoeff f) := by simp

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