theorem Ideal.fg_span_iff_fg_span_finset_subset {R : Type u_1} [Semiring R] (s : Set R) : (span s).FG ↔ ∃ (s' : Finset R), ↑s' ⊆ s ∧ span s = span ↑s'

A subset $s \subseteq R$ has finitely generated span if and only if: $\exists$ finite $s' \subseteq s$ such that $\mathsf{span}(s) = \mathsf{span}(s')$

@[simp]

theorem Ideal.span_singleton_zero {R : Type u_1} [Semiring R] : span {0} = ⊥

For any ring $R$, the span of the zero singleton set equals the zero submodule: $$ \mathsf{span}_R \{(0 : R)\} = \bot $$

@[simp]

theorem Ideal.span_insert_zero {R : Type u_1} [Semiring R] (s : Set R) : span (insert 0 s) = span s

For any subset $s \subseteq R$ of a ring $R$, inserting zero does not change the linear span: $$ \mathsf{span}_R(\{0\} \cup s) = \mathsf{span}_R(s) $$

@[simp]

theorem Ideal.span_sdiff_singleton_zero {R : Type u_1} [Semiring R] (s : Set R) : span (s \ {0}) = span s

For any subset $s \subseteq R$ of a ring $R$, removing zero does not change the linear span: $$ \mathsf{span}_R(s \setminus \{0\}) = \mathsf{span}_R(s) $$

theorem MonomialOrder.leadingTerm_ideal_span_monomial {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_3} [CommSemiring R] {B : Set (MvPolynomial σ R)} (hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)) : Ideal.span (m.leadingTerm '' B) = Ideal.span ((fun (p : MvPolynomial σ R) => (MvPolynomial.monomial (m.degree p)) 1) '' B)

Let $G'' \subseteq R[x_1, \dots, x_n]$ be a set of polynomials such that $$ \forall p \in G'',\ \operatorname{leadingCoeff}(p) \in R^\times. $$ Then, $$ \left\langle \operatorname{lt}(G'') \right\rangle = \left\langle x^{\deg(p)} \mid p \in G'' \right\rangle, $$

theorem MonomialOrder.leadingTerm_ideal_sdiff_singleton_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_3} [CommSemiring R] (B : Set (MvPolynomial σ R)) : Ideal.span (m.leadingTerm '' (B \ {0})) = Ideal.span (m.leadingTerm '' B)

theorem MonomialOrder.leadingTerm_ideal_insert_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_3} [CommSemiring R] (B : Set (MvPolynomial σ R)) : Ideal.span (m.leadingTerm '' insert 0 B) = Ideal.span (m.leadingTerm '' B)

theorem MonomialOrder.IsGroebnerBasis_erase_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_3} [CommSemiring R] (G : Finset (MvPolynomial σ R)) (I : Ideal (MvPolynomial σ R)) : m.IsGroebnerBasis (G.erase 0) I ↔ m.IsGroebnerBasis G I

theorem MonomialOrder.IsGroebnerBasis_union_singleton_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_3} [CommSemiring R] (G : Finset (MvPolynomial σ R)) (I : Ideal (MvPolynomial σ R)) : m.IsGroebnerBasis (G ∪ {0}) I ↔ m.IsGroebnerBasis G I

theorem MonomialOrder.leadingTerm_ideal_span_monomial' {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_2} [Field k] (B : Set (MvPolynomial σ k)) : Ideal.span (m.leadingTerm '' B) = Ideal.span ((fun (p : MvPolynomial σ k) => (MvPolynomial.monomial (m.degree p)) 1) '' (B \ {0}))

$$ \langle \mathrm{lt}(G) \rangle = \left\langle \left\{ x^t : t \in \{ \mathrm{multideg}(p) : p \in G \setminus \{0\} \} \right\} \right\rangle $$

theorem MonomialOrder.mem_ideal_of_remainder_mem_ideal {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_3} [CommSemiring R] {B : Set (MvPolynomial σ R)} {r : MvPolynomial σ R} {I : Ideal (MvPolynomial σ R)} {p : MvPolynomial σ R} (hBI : B ⊆ ↑I) (hpBr : m.IsRemainder p B r) (hr : r ∈ I) : p ∈ I

Let $G'' \subseteq R[x_1, \dots, x_n]$, let $I \subseteq R[x_1, \dots, x_n]$ be an ideal, and let $p, r \in R[x_1, \dots, x_n]$. Suppose that:

• $G'' \subseteq I$,
• $r \in I$,
• $r$ is the remainder of $p$ upon division by $G''$.

Then, $$ p \in I. $$

theorem MonomialOrder.remainder_mem_ideal_iff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_4} [CommRing R] {B : Set (MvPolynomial σ R)} {r : MvPolynomial σ R} {I : Ideal (MvPolynomial σ R)} {p : MvPolynomial σ R} (hBI : B ⊆ ↑I) (hpBr : m.IsRemainder p B r) : r ∈ I ↔ p ∈ I

Let $R$ be a commutative ring, and let $G'' \subseteq R[x_1, \dots, x_n]$, $I \subseteq R[x_1, \dots, x_n]$ be an ideal, and $p, r \in R[x_1, \dots, x_n]$. Assume that:

• $G'' \subseteq I$,
• $r$ is the remainder of $p$ upon division by $G''$.

Then, $$ r \in I \quad \Longleftrightarrow \quad p \in I. $$

theorem MonomialOrder.remainder_sub_remainder_mem_ideal {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_4} [CommRing R] {B : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} {p r₁ r₂ : MvPolynomial σ R} (hBI : B ⊆ ↑I) (hr₁ : m.IsRemainder p B r₁) (hr₂ : m.IsRemainder p B r₂) : r₁ - r₂ ∈ I

Let $I \subseteq k[x_i : i \in \sigma]$ be an ideal, and let $G \subseteq I$ be a finite subset. Suppose that $r_1$ and $r_2$ are generalized remainders of a polynomial $p$ upon division by $G$. Then, $$ r_1 - r_2 \in I. $$

theorem MonomialOrder.IsRemainder_term_not_mem_leading_term_ideal {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_3} [CommSemiring R] {p r : MvPolynomial σ R} {B : Set (MvPolynomial σ R)} (hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)) (h : m.IsRemainder p B r) (s : σ →₀ ℕ) : s ∈ r.support → (MvPolynomial.monomial s) (MvPolynomial.coeff s r) ∉ Ideal.span (m.leadingTerm '' B)

theorem MonomialOrder.IsRemainder_term_not_mem_leading_term_ideal' {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_2} [Field k] {p r : MvPolynomial σ k} {B : Set (MvPolynomial σ k)} (h : m.IsRemainder p B r) (s : σ →₀ ℕ) : s ∈ r.support → (MvPolynomial.monomial s) (MvPolynomial.coeff s r) ∉ Ideal.span (m.leadingTerm '' B)

theorem MonomialOrder.IsRemainder_monomial_not_mem_leading_term_ideal {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_3} [CommSemiring R] {p r : MvPolynomial σ R} {B : Set (MvPolynomial σ R)} (hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)) (h : m.IsRemainder p B r) (s : σ →₀ ℕ) : s ∈ r.support → (MvPolynomial.monomial s) 1 ∉ Ideal.span (m.leadingTerm '' B)

theorem MonomialOrder.IsRemainder_monomial_not_mem_leading_term_ideal' {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_2} [Field k] {p r : MvPolynomial σ k} {B : Set (MvPolynomial σ k)} (h : m.IsRemainder p B r) (s : σ →₀ ℕ) : s ∈ r.support → (MvPolynomial.monomial s) 1 ∉ Ideal.span (m.leadingTerm '' B)