homothetyHom — Mathlib

English

The construction homothetyAffine c is an affine map from k to affine endomorphisms of P1 that sends r to the affine map homothety c r.

Русский

Конструкция homothetyAffine c представляет собой аффинное отображение из поля k в аффинные отображения P1→P1, которое отправляет r в отображение homothety c r.

LaTeX

$$$\text{homothetyAffine}(c) : k \to^\mathrm{aff} (P_1 \to^\mathrm{aff} P_1)$ с таким свойством, что $\text{toFun}(r)=\operatorname{homothety}(c,r)$$$

Lean4

/-- `homothety` as a multiplicative monoid homomorphism. -/
def homothetyHom (c : P1) : k →* P1 →ᵃ[k] P1 where
  toFun := homothety c
  map_one' := homothety_one c
  map_mul' := homothety_mul c

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