coe_homothetyHom — Mathlib

English

The underlying function of the monoid homomorphism homothetyHom c is exactly the map homothety c.

Русский

Функциональное отображение моноид-гомоморфизма homothetyHom c совпадает с отображением homothety c.

LaTeX

$$$\forall r\in k,\ (\operatorname{homothetyHom}(c))(r) = \operatorname{homothety}(c,r)$$$

Lean4

@[simp]
theorem coe_homothetyHom (c : P1) : ⇑(homothetyHom c : k →* _) = homothety c :=
  rfl

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