lengthParity_comp_simple — Mathlib

English

The parity map composed with the simple generator map equals the constant parity 1; i.e., lengthParity ∘ simple = a constant map to 1.

Русский

Пусть длина в составе simple имеет постоянный паритет 1: lengthParity ∘ simple = константа 1.

LaTeX

$$$$ (\\\\text{lengthParity} \\\\circ \\\\text{simple})(i) = 1 \\\\text{ for all } i \\\\in B $$$$

Lean4

theorem lengthParity_comp_simple : cs.lengthParity ∘ cs.simple = fun _ ↦ Multiplicative.ofAdd 1 :=
  funext cs.lengthParity_simple

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