homothety_def — Mathlib

English

The homothetyHom and homothetyAffine constructions package the scalar-to-endomorphism correspondence: a monoid homomorphism sending r to the affine map homothety c r.

Русский

Конструкция homothetyAffine описывает гомотетию как отображение из коэффициента r в аффинное самонаправление: отображение $r \mapsto \mathrm{homothety}(c,r)$.

LaTeX

$$$\text{HomothetyAffine}(c) : k \to^\mathrm{aff} P_1 \to^\mathrm{aff} P_1$, тривиально задаётся через $r \mapsto \mathrm{homothety}(c,r)$.$$

Lean4

theorem homothety_def (c : P1) (r : k) : homothety c r = r • (id k P1 -ᵥ const k P1 c) +ᵥ const k P1 c :=
  rfl

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