toAffineMap_injective — Mathlib

English

The map e ↦ e.toAffineMap is injective; distinct affine equivalences give distinct affine maps.

Русский

Отображение e ↦ e.toAffineMap инъективно: разные аффинные эквиваленты соответствуют разным аффинным картам.

LaTeX

$$$\\forall e,e',\\; e.toAffineMap = e'.toAffineMap \\Rightarrow e = e'$$$

Lean4

theorem toAffineMap_injective : Injective (toAffineMap : (P₁ ≃ᵃ[k] P₂) → P₁ →ᵃ[k] P₂) :=
  by
  rintro ⟨e, el, h⟩ ⟨e', el', h'⟩ H
  simp_all

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