Theorems · Theorem · commutative algebra

MonomialOrder.span_leadingTerm_eq_span_monomial

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

Defined in: Mathlib.RingTheory.MvPolynomial.Ideal
Cited by: 1 results in Mathlib
Foundations: Depth 86 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommSemiring

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites32

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Setstatement and proof · cited by 53,352
RingHom.idstatement · cited by 18,349
CommSemiringstatement and proof · cited by 10,911
LinearMapstatement · cited by 10,215
Set.imagestatement and proof · cited by 5,609
Finsuppstatement · cited by 5,255
Idealstatement and proof · cited by 4,748
one_mulproof · cited by 2,841
MvPolynomialstatement and proof · cited by 2,140
le_antisymmproof · cited by 2,068
Units.valproof · cited by 1,966

Cited by1

Results whose statement or proof uses this declaration.

MonomialOrder.span_leadingTerm_eq_span_monomial₀proof · cited by 1