toAffineMap_inj

Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

URI: https://scilib.ai/kg/mathlib#AffineEquiv.toAffineMap_inj

English

The equality e.toAffineMap = e'.toAffineMap is equivalent to e = e'.

Русский

Равенство e.toAffineMap = e'.toAffineMap эквивалентно e = e'.

LaTeX

$$$e.toAffineMap = e'.toAffineMap \\iff e = e'$$$

Lean4

@[simp]
theorem toAffineMap_inj {e e' : P₁ ≃ᵃ[k] P₂} : e.toAffineMap = e'.toAffineMap ↔ e = e' :=
  toAffineMap_injective.eq_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru