length_simple — Mathlib

English

If s_i is a simple reflection corresponding to i, then its length is exactly 1: ℓ(s_i) = 1.

Русский

Длина простого отражения s_i равна 1: ℓ(s_i) = 1.

LaTeX

$$$\\\\ell(s_i) = 1$$$

Lean4

@[simp]
theorem length_simple (i : B) : ℓ(s i) = 1 := by
  apply Nat.le_antisymm
  · simpa using cs.length_wordProd_le [i]
  · by_contra! length_lt_one
    have : cs.lengthParity (s i) = Multiplicative.ofAdd 0 := by
      rw [lengthParity_eq_ofAdd_length, Nat.lt_one_iff.mp length_lt_one, Nat.cast_zero]
    have : Multiplicative.ofAdd (0 : ZMod 2) = Multiplicative.ofAdd 1 := this.symm.trans (cs.lengthParity_simple i)
    contradiction

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