degreesLE_add — Mathlib

English

The DegreesLE construction respects addition in the sense that the degree bound for a sum is controlled by the sum of bounds.

Русский

Конструкция DegreesLE сохраняет аддитивность: граница степеней суммы управляется суммой ограничений.

LaTeX

$$$\\\\operatorname{degreesLE}(R,\\\\sigma, s+t) = \\\\operatorname{degreesLE}(R,\\\\sigma, s) \\\\cdot \\\\operatorname{degreesLE}(R,\\\\sigma, t)$$$

Lean4

theorem degreesLE_add : degreesLE R σ (s + t) = degreesLE R σ s * degreesLE R σ t := by
  classical
  rw [le_antisymm_iff, Submodule.mul_le]
  refine ⟨fun x hx ↦ x.as_sum ▸ sum_mem fun i hi ↦ ?_, fun x hx y hy ↦ degrees_mul_le.trans (add_le_add hx hy)⟩
  replace hi : i.toMultiset ≤ s + t := (Finset.le_sup hi).trans hx
  let a := (i.toMultiset - t).toFinsupp
  let b := (i.toMultiset ⊓ t).toFinsupp
  have : a + b = i := Multiset.toFinsupp.symm.injective (by simp [a, b, Multiset.sub_add_inter])
  have ha : a.toMultiset ≤ s := by simpa [a, add_comm (a := t)] using hi
  have hb : b.toMultiset ≤ t := by simp [b, Multiset.inter_le_right]
  rw [show monomial i (x.coeff i) = monomial a (x.coeff i) * monomial b 1 by simp [this]]
  exact Submodule.mul_mem_mul ((degrees_monomial _ _).trans ha) ((degrees_monomial _ _).trans hb)

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