English
The homothetyAffine c is the affine map from k to the space of affine self-maps of P1 that sends r to homothety c r.
Русский
HomothetyAffine c — это аффинное отображение из поля k в множество аффинных самоперобразований P1, отправляющее r в homothety(c,r).
LaTeX
$$$\operatorname{homothetyAffine}(c) : k \to^\mathrm{aff} (P_1 \to^\mathrm{aff} P_1)$ с $\operatorname{toFun}(r)=\operatorname{homothety}(c,r)$$$
Lean4
instance toAddTorsor (s : AffineSubspace k P) [Nonempty s] : AddTorsor s.direction s
where
vadd a b := ⟨(a : V) +ᵥ (b : P), vadd_mem_of_mem_direction a.2 b.2⟩
zero_vadd := fun a => by
ext
exact zero_vadd _ _
add_vadd a b
c := by
ext
apply add_vadd
vsub a b := ⟨(a : P) -ᵥ (b : P), (vsub_left_mem_direction_iff_mem a.2 _).mpr b.2⟩
vsub_vadd' a
b := by
ext
apply AddTorsor.vsub_vadd'
vadd_vsub' a
b := by
ext
apply AddTorsor.vadd_vsub'
