length_mul_left_ne — Mathlib

English

If t is a reflection, then for every w in the group, the Coxeter length of w t differs from that of w.

Русский

Если t — отражение, то для любого w в группе ℝ, длина ℓ(w t) отличается от ℓ(w).

LaTeX

$$$cs.IsReflection\, t \rightarrow \forall w:\, W, \ell(w t) \neq \ell(w)$$$

Lean4

theorem length_mul_left_ne (w : W) : ℓ(w * t) ≠ ℓ w :=
  by
  suffices cs.lengthParity (w * t) ≠ cs.lengthParity w
    by
    contrapose! this
    simp only [lengthParity_eq_ofAdd_length, this]
  rcases ht with ⟨w, i, rfl⟩
  simp [lengthParity_simple]

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