coe_homothetyUnitsMulHom_apply — Mathlib

English

The action of a unit t on the space via homothety with center p is exactly the corresponding affine map homothety.

Русский

Действие единицы t на пространство через гомотетию с центром p совпадает с соответствующим аффинным преобразованием гомотетии.

LaTeX

$$(homothetyUnitsMulHom p t : P → P) = AffineMap.homothety p (t : R)$$

Lean4

@[simp]
theorem coe_homothetyUnitsMulHom_apply (p : P) (t : Rˣ) :
    (homothetyUnitsMulHom p t : P → P) = AffineMap.homothety p (t : R) :=
  rfl

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