homothety_linear — Mathlib

English

The linear part of the affine map homothety c r is r times the identity map.

Русский

Линейная часть аффинного отображения гомотетии равна r умножению на тождественное отображение.

LaTeX

$$$\big(\operatorname{homothety}(c,r)\big)^{\text{linear}} = r \cdot \mathrm{Id}$$$

Lean4

@[simp]
theorem homothety_linear (c : P1) (r : k) : (homothety c r).linear = r • LinearMap.id := by simp [homothety]

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