English
The parity-graded submodules multiply compatibly: the product of elements from the i-th and j-th components lies in the (i+j)-th component, i.e., evenOdd(Q,i) · evenOdd(Q,j) ≤ evenOdd(Q,i+j).
Русский
Произведение элементов из i-й и j-й компоненты градации лежит в i+j-й компоненте: evenOdd(Q,i)·evenOdd(Q,j) ≤ evenOdd(Q,i+j).
LaTeX
$$$\\mathrm{evenOdd}(Q,i) \\cdot \\mathrm{evenOdd}(Q,j) \\le \\mathrm{evenOdd}(Q,i+j)$$$
Lean4
theorem evenOdd_mul_le (i j : ZMod 2) : evenOdd Q i * evenOdd Q j ≤ evenOdd Q (i + j) :=
by
simp_rw [evenOdd, Submodule.iSup_eq_span, Submodule.span_mul_span]
apply Submodule.span_mono
simp_rw [Set.iUnion_mul, Set.mul_iUnion, Set.iUnion_subset_iff, Set.mul_subset_iff]
rintro ⟨xi, rfl⟩ ⟨yi, rfl⟩ x hx y hy
refine Set.mem_iUnion.mpr ⟨⟨xi + yi, Nat.cast_add _ _⟩, ?_⟩
simp only [pow_add]
exact Submodule.mul_mem_mul hx hy
