length_inv — Mathlib

English

For every w in W, the length is unchanged by taking inverses: ℓ(w⁻¹) = ℓ(w).

Русский

Для каждого w в W длина сохраняется при взятии обратного: ℓ(w⁻¹) = ℓ(w).

LaTeX

$$$\\\\ell(w^{-1}) = \\\\ell(w)$$$

Lean4

@[simp]
theorem length_inv (w : W) : ℓ(w⁻¹) = ℓ w := by
  apply Nat.le_antisymm
  · rcases cs.exists_reduced_word w with ⟨ω, hω, rfl⟩
    have := cs.length_wordProd_le (List.reverse ω)
    rwa [wordProd_reverse, length_reverse, hω] at this
  · rcases cs.exists_reduced_word w⁻¹ with ⟨ω, hω, h'ω⟩
    have := cs.length_wordProd_le (List.reverse ω)
    rwa [wordProd_reverse, length_reverse, ← h'ω, hω, inv_inv] at this

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