length_mul_right_ne — Mathlib

English

If t is a reflection, then for every w, ℓ(t w) ≠ ℓ w.

Русский

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

LaTeX

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

Lean4

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

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