coroot'_reflectionPerm — Mathlib

English

For i, j ∈ ι, the coroot corresponding to the reflectionPerm(i, j) equals the composition coroot'(j) ∘ reflection i: coroot'(P.reflectionPerm(i,j)) = coroot'(j) ∘ P.reflection(i).

Русский

Для i, j ∈ ι сопряжённая корота к отражению Perm(i, j) равна композиции coroot'(j) и отражения i: coroot'(P.reflectionPerm(i,j)) = coroot'(j) ∘ reflection(i).

LaTeX

$$$ P.coroot'(P.reflectionPerm(i,j)) = P.coroot'(j) \circ P.reflection(i) $$$

Lean4

theorem coroot'_reflectionPerm {i j : ι} : P.coroot' (P.reflectionPerm i j) = P.coroot' j ∘ₗ P.reflection i :=
  by
  ext y
  simp [coreflection_apply_coroot, reflection_apply, map_sub, mul_comm]

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