length_simple_mul — Mathlib

English

There is a dichotomy: either ℓ(w s_i) = ℓ(w) + 1 or ℓ(w s_i) + 1 = ℓ(w).

Русский

Существует либо ℓ(w s_i) = ℓ(w) + 1, либо ℓ(w s_i) + 1 = ℓ(w).

LaTeX

$$$$ \ell(w s_i) = \ell(w) + 1 \quad \\text{or} \quad \ell(w s_i) + 1 = \ell(w) $$$$

Lean4

theorem length_simple_mul (w : W) (i : B) : ℓ(s i * w) = ℓ w + 1 ∨ ℓ(s i * w) + 1 = ℓ w :=
  by
  have := cs.length_mul_simple w⁻¹ i
  rwa [(by simp : w⁻¹ * (s i) = ((s i) * w)⁻¹), length_inv, length_inv] at this

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