English
The degrees bound by a sum multiset satisfy a product relation: degreesLE(s+t) equals degreesLE(s) times degreesLE(t).
Русский
Пределы степеней, ограниченные суммой multisets, удовлетворяют отношению произведения: degreesLE(s+t) = degreesLE(s) · degreesLE(t).
LaTeX
$$$\\\\operatorname{degreesLE} (R,\\\\sigma, s+t) = \\\\operatorname{degreesLE} (R,\\\\sigma, s) \\\\cdot \\\\operatorname{degreesLE} (R,\\\\sigma, t)$$$
Lean4
/-- The submodule of multivariate polynomials of degrees bounded by a monomial `s`. -/
def degreesLE : Submodule R (MvPolynomial σ R)
where
carrier := {p | p.degrees ≤ s}
add_mem' {a b} ha hb := by classical exact degrees_add_le.trans (sup_le ha hb)
zero_mem' := by simp
smul_mem' c {x}
hx := by
dsimp
rw [Algebra.smul_def]
refine degrees_mul_le.trans ?_
simpa [degrees_C] using hx
