rescale_rescale — Mathlib

English

Rescaling by b after a is the same as rescaling by a·b: rescale b (rescale a f) = rescale (a b) f.

Русский

После масштабирования на a следует масштабирование на b, что эквивалентно масштабированию на a·b: rescale b (rescale a f) = rescale (a b) f.

LaTeX

$$$\mathrm{rescale}\, b\, (\mathrm{rescale}\, a\, f) = \mathrm{rescale}\, (a b)\, f$$$

Lean4

theorem rescale_rescale (f : R⟦X⟧) (a b : R) : rescale b (rescale a f) = rescale (a * b) f :=
  by
  ext n
  simp_rw [coeff_rescale]
  rw [mul_pow, mul_comm _ (b ^ n), mul_assoc]

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