coreflection_inv

Mathlib.LinearAlgebra.RootSystem.Defs

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

English

The inverse of coreflection is itself.

Русский

Обратная coreflection равна самой coreflection.

LaTeX

$$$ (P.coreflection(i))^{-1} = P.coreflection(i) $$$

Lean4

@[simp]
theorem coreflection_inv : (P.coreflection i)⁻¹ = P.coreflection i :=
  rfl

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

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

Разделы

Аффилиация

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