English
For any coefficient submodule M and any polynomial p in the multivariate polynomial ring with variables σ over S, multiplying p by a monomial of the form monomial i 1 does not change membership in the submodule of polynomials whose coefficients lie in M. In symbols, monomial i 1 · p ∈ coeffsIn(σ, M) iff p ∈ coeffsIn(σ, M).
Русский
Для любой подмодуля коэффициентов M и любого многочлена p из полиномного кольца с переменными σ над S умножение p на мономиал вида monomial i 1 не меняет принадлежность подмножеству coeffsIn(σ, M). То есть monomial i 1 · p ∈ coeffsIn(σ, M) тогда и только тогда, когда p ∈ coeffsIn(σ, M).
LaTeX
$$$\\operatorname{monomial}(i,1)\\cdot p \\in \\operatorname{coeffsIn}(\\sigma,M) \\iff p \\in \\operatorname{coeffsIn}(\\sigma,M)$$$
Lean4
@[simp]
theorem monomial_mul_mem_coeffsIn : monomial i 1 * p ∈ coeffsIn σ M ↔ p ∈ coeffsIn σ M := by simp [mul_comm]
