English
The map coeffsIn is multiplicative with respect to submodule multiplication: coeffsIn σ (M * N) = coeffsIn σ M * coeffsIn σ N.
Русский
Отображение coeffsIn сохраняет умножение подмодулей: coeffsIn σ (M * N) = coeffsIn σ M * coeffsIn σ N.
LaTeX
$$$\\operatorname{coeffsIn}(\\sigma, M \\cdot N) = \\operatorname{coeffsIn}(\\sigma, M) \\cdot \\operatorname{coeffsIn}(\\sigma, N)$$$
Lean4
theorem coeffsIn_mul (M N : Submodule R S) : coeffsIn σ (M * N) = coeffsIn σ M * coeffsIn σ N := by
classical
refine le_antisymm (coeffsIn_le.2 ?_) ?_
· intro r hr s
induction hr using Submodule.mul_induction_on' with
| mem_mul_mem m hm n hn =>
rw [← add_zero s, ← monomial_mul]
apply Submodule.mul_mem_mul <;> simpa
| add x _ y _ hx hy => simpa [map_add] using add_mem hx hy
· rw [Submodule.mul_le]
intro x hx y hy k
rw [MvPolynomial.coeff_mul]
exact sum_mem fun c hc ↦ Submodule.mul_mem_mul (hx _) (hy _)
