instCoeAffineMap — Mathlib

English

Affine equivalences can be viewed as affine maps via a canonical coe; there is a natural coercion from affine equivalences to affine maps.

Русский

Аффинные эквивалентности могут рассматриваться как аффинные отображения через каноническое преобразование; существует естественное вложение из аффинных эквивалентностей в аффинные отображения.

LaTeX

$$$e \mapsto e.toAffineMap \in \mathrm{AffineMap}(k;P_1,P_2)$$$

Lean4

instance : Coe (P₁ ≃ᵃ[k] P₂) (P₁ →ᵃ[k] P₂) :=
  ⟨toAffineMap⟩

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