toEquiv_pointReflection

Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

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

English

Applying the point reflection twice yields the identity map.

Русский

Применение точечного отражения дважды даёт тождественное отображение.

LaTeX

$$(pointReflection(k,x))^2 = id$$

Lean4

@[simp]
theorem toEquiv_pointReflection (x : P₁) : (pointReflection k x).toEquiv = Equiv.pointReflection x :=
  rfl

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

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

Разделы

Аффилиация

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