reflectionPerm_eq_iff_smul_root — Mathlib

English

The condition reflectionPerm i j = j is equivalent to pairing j i · root i = 0.

Русский

Условие reflectionPerm i j = j эквивалентно pairing j i · root i = 0.

LaTeX

$$$$ P.reflectionPerm(i,j) = j \\iff P.pairing(j,i) \\cdot P.root(i) = 0. $$$$

Lean4

theorem reflectionPerm_eq_iff_smul_root : P.reflectionPerm i j = j ↔ P.pairing j i • P.root i = 0 :=
  ⟨fun h ↦ by simpa [h] using P.reflectionPerm_root i j, fun h ↦ P.root.injective <| by simp [reflection_apply, h]⟩

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