homothety_mul_apply — Mathlib

English

For all c, r1, r2, p, homothety c (r1 r2) p = homothety c r1 (homothety c r2 p).

Русский

Для всех c, r1, r2, p: homothety c (r1 r2) p = homothety c r1 (homothety c r2 p).

LaTeX

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

Lean4

theorem homothety_mul_apply (c : P1) (r₁ r₂ : k) (p : P1) :
    homothety c (r₁ * r₂) p = homothety c r₁ (homothety c r₂ p) := by simp only [homothety_apply, mul_smul, vadd_vsub]

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