symm_trans_self

Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

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

English

For an affine equivalence e: P1 ≃ᵃ[k] P2, composing its inverse with itself yields the identity on P2: e^{-1} ∘ e = id.

Русский

Для аффинного эквивалента e: P1 ≃ᵃ[k] P2 композиция e^{-1} с e даёт тождество на P2: e^{-1} ∘ e = id.

LaTeX

$$$e^{-1} \circ e = \mathrm{id}_{P_2}$$$

Lean4

@[simp]
theorem symm_trans_self (e : P₁ ≃ᵃ[k] P₂) : e.symm.trans e = refl k P₂ :=
  ext e.apply_symm_apply

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

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

Разделы

Аффилиация

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