reflectionPerm_eq_reflectionPerm_iff

English

For a RootSystem P and indices i, j, P.reflectionPerm i = P.reflectionPerm j if and only if P.reflection i = P.reflection j.

Русский

Для корневой системы P и индексов i, j верно: P.reflectionPerm i = P.reflectionPerm j тогда и только тогда, когда P.reflection i = P.reflection j.

LaTeX

$$$$ P.reflectionPerm i = P.reflectionPerm j \\iff P.reflection i = P.reflection j. $$$$

Lean4

theorem _root_.RootSystem.reflectionPerm_eq_reflectionPerm_iff (P : RootSystem ι R M N) (i j : ι) :
    P.reflectionPerm i = P.reflectionPerm j ↔ P.reflection i = P.reflection j :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ Equiv.ext fun k ↦ P.root.injective <| by simp [h]⟩
  ext x
  exact (P.reflectionPerm_eq_reflectionPerm_iff_of_span i j).mp h x <| by simp

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