coreflection_same

Mathlib.LinearAlgebra.RootSystem.Defs

URI: https://scilib.ai/kg/mathlib#RootPairing.coreflection_same

English

The coreflection of i has square equal to identity on N.

Русский

Квадрат coreflection i равен тождественному отображению на N.

LaTeX

$$$ P.coreflection(i)^{2} = \mathrm{id}_N $$$

Lean4

@[simp]
theorem coreflection_same (x : N) : P.coreflection i (P.coreflection i x) = x :=
  Module.involutive_reflection (P.flip.coroot_root_two i) x

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

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

Разделы

Аффилиация

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