rescale_zero — Mathlib

English

Rescale by zero equals the composition of the constant-coefficient series with the constant term operator.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem rescale_zero : rescale 0 = (C (R := R)).comp constantCoeff :=
  by
  ext x n
  simp only [Function.comp_apply, RingHom.coe_comp, rescale, RingHom.coe_mk, coeff_C]
  split_ifs with h <;> simp [h]

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