reflection_mul_reflection

Mathlib.Analysis.InnerProductSpace.Projection.Reflection

URI: https://scilib.ai/kg/mathlib#Submodule.reflection_mul_reflection

English

As above, composition of reflections yields identity when composed with itself.

Русский

Как и ранее, композиция отражений дает тождество при повторном применении.

LaTeX

$$$K.reflection \\circ K.reflection = \\mathrm{Id}$$$

Lean4

/-- Reflection is involutive. -/
@[simp]
theorem reflection_mul_reflection : K.reflection * K.reflection = 1 :=
  reflection_trans_reflection _

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

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

Разделы

Аффилиация

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