homothetyAffine — Mathlib

English

The coe of the affine map homothetyAffine c equals the function homothety c.

Русский

Коэрция аффинного отображения homothetyAffine c равна функции homothety c.

LaTeX

$$$\forall r,\ \text{coe}(\mathrm{homothetyAffine}(c))(r) = \mathrm{homothety}(c,r)$$$

Lean4

/-- `homothety` as an affine map. -/
def homothetyAffine (c : P1) : k →ᵃ[k] P1 →ᵃ[k] P1 :=
  ⟨homothety c, (LinearMap.lsmul k _).flip (id k P1 -ᵥ const k P1 c), Function.swap (homothety_add c)⟩

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