length_mul_mod_two — Mathlib

English

The parity of the product equals the sum of parities: ℓ(w1 w2) mod 2 = (ℓ(w1) + ℓ(w2)) mod 2.

Русский

Паритет длины произведения равен сумме паритетов длин: ℓ(w1 w2) ≡ ℓ(w1) + ℓ(w2) (mod 2).

LaTeX

$$$$ \\ell(w_1 w_2) \\\\mod 2 = (\\\\ell(w_1) + \\\\ell(w_2)) \\\\mod 2 $$$$

Lean4

theorem length_mul_mod_two (w₁ w₂ : W) : ℓ(w₁ * w₂) % 2 = (ℓ w₁ + ℓ w₂) % 2 :=
  by
  rw [← ZMod.natCast_eq_natCast_iff', Nat.cast_add]
  simpa only [lengthParity_eq_ofAdd_length, ofAdd_add] using map_mul cs.lengthParity w₁ w₂

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