pairing_reflectionPerm — Mathlib

English

For i, j, k ∈ ι, the pairing satisfies j with reflectionPerm(i, k) equals pairing with reflectionPerm(i, j) and k: pairing j (reflectionPerm i k) = pairing (reflectionPerm i j) k.

Русский

Для i, j, k ∈ ι паринг удовлетворяет: pairing(j, reflectionPerm(i, k)) = pairing(reflectionPerm(i, j), k).

LaTeX

$$$ P.pairing(j, P.reflectionPerm(i,k)) = P.pairing(P.reflectionPerm(i,j), k) $$$

Lean4

theorem pairing_reflectionPerm (i j k : ι) : P.pairing j (P.reflectionPerm i k) = P.pairing (P.reflectionPerm i j) k :=
  by
  simp only [pairing, root', coroot_reflectionPerm, root_reflectionPerm]
  simp [coreflection_apply_coroot, reflection_apply_root, mul_comm]

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