pairing_smul_root_eq — Mathlib

English

If reflectionPerm i = reflectionPerm j, then P.pairing k i · root i = P.pairing k j · root j.

Русский

Если reflectionPerm i = reflectionPerm j, то pairing k i · root i = pairing k j · root j.

LaTeX

$$$ P.pairing(k,i) \cdot P.root(i) = P.pairing(k,j) \cdot P.root(j) $$$

Lean4

theorem pairing_smul_root_eq (k : ι) (hij : P.reflectionPerm i = P.reflectionPerm j) :
    P.pairing k i • P.root i = P.pairing k j • P.root j :=
  by
  have h : P.reflection i (P.root k) = P.reflection j (P.root k) := by simp only [← root_reflectionPerm, hij]
  simpa only [reflection_apply_root, sub_right_inj] using h

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