lengthParity_simple — Mathlib

English

For every generator i in B, the parity of the length of the corresponding simple reflection s_i is odd: lengthParity(s_i) = 1.

Русский

Для каждого основания i в B параитет длины простого отражения s_i равен единице: lengthParity(s_i) = 1.

LaTeX

$$$\\\\ell(s_i) \\\\text{mod } 2 = 1$$$

Lean4

theorem lengthParity_simple (i : B) : cs.lengthParity (s i) = Multiplicative.ofAdd 1 :=
  cs.lift_apply_simple _ _

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