homothety_mul — Mathlib

English

Homothety with product of scales equals the composition of homotheties with each scale.

Русский

Гомотетия с коэффициентом r1 r2 равна композиции гомотетий с r1 и r2.

LaTeX

$$$\operatorname{homothety}(c, r_1 r_2) = (\operatorname{homothety}(c, r_1))\circ (\operatorname{homothety}(c, r_2))$$$

Lean4

theorem homothety_mul (c : P1) (r₁ r₂ : k) : homothety c (r₁ * r₂) = (homothety c r₁).comp (homothety c r₂) :=
  ext <| homothety_mul_apply c r₁ r₂

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