rescale_mul — Mathlib

English

Rescale by a·b equals the composition of rescale by b after rescale by a: rescale(a b) = (rescale b) ∘ (rescale a).

Русский

Масштабирование на a·b равно композиции масштабирования на a и затем на b: rescale(a b) = (rescale b) ∘ (rescale a).

LaTeX

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

Lean4

theorem rescale_mul (a b : R) : rescale (a * b) = (rescale b).comp (rescale a) :=
  by
  ext
  simp [← rescale_rescale]

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