toEquiv_inj

Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

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

English

A simplification of the statement that equality of toEquiv implies equality of the affine equivalences.

Русский

Упрощение утверждения: равенство toEquiv влечет равенство аффинных эквивалентностей.

LaTeX

$$$e.toEquiv = e'.toEquiv \Rightarrow e = e'$$$

Lean4

@[simp]
theorem toEquiv_inj {e e' : P₁ ≃ᵃ[k] P₂} : e.toEquiv = e'.toEquiv ↔ e = e' :=
  toEquiv_injective.eq_iff

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

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

Разделы

Аффилиация

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