pairing_smul_coroot_eq — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem pairing_smul_coroot_eq (k : ι) (hij : P.reflectionPerm i = P.reflectionPerm j) :
    P.pairing i k • P.coroot i = P.pairing j k • P.coroot j :=
  by
  have h : P.coreflection i (P.coroot k) = P.coreflection j (P.coroot k) := by simp only [← coroot_reflectionPerm, hij]
  simpa only [coreflection_apply_coroot, sub_right_inj] using h

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