symm_trans_self

Mathlib.Analysis.Normed.Affine.Isometry

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

English

For an affine isometry e, composing with its inverse in the other order yields the identity on P₂.

Русский

Для аффинной изометрии e композиция e.symm.trans e даёт тождество на P₂.

LaTeX

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

Lean4

@[simp]
theorem symm_trans_self : e.symm.trans e = refl 𝕜 P₂ :=
  ext e.apply_symm_apply

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

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

Разделы

Аффилиация

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