reflection — Mathlib

English

The root after applying the reflection permutation equals the reflected root: root(reflectionPerm i j) = reflection(i)(root j).

Русский

Корень после применения отражения перестановки равен отражённому корню: root(reflectionPerm i j) = reflection(i)(root j).

LaTeX

$$$ \mathrm{root}(\mathrm{reflectionPerm}(i,j)) = (\mathrm{reflection}(i))(\mathrm{root}(j)) $$$

Lean4

/-- The reflection associated to a root. -/
def reflection : M ≃ₗ[R] M :=
  Module.reflection (P.flip.root_coroot_two i)

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