Theorems · Definition · commutative algebra
MonomialOrder.toSyn
{σ : Type u_1} → (self : MonomialOrder σ) → (σ →₀ ℕ) ≃+ self.synthe additive equivalence from σ →₀ ℕ to syn
- Defined in
- Mathlib.Data.Finsupp.MonomialOrder
- Cited by
- 82 results in Mathlib
- Foundations
- Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsuppstatement · cited by 5,255
- AddEquivstatement · cited by 1,087
- MonomialOrderstatement and proof · cited by 199
- MonomialOrder.synstatement · cited by 85
Cited by85
Results whose statement or proof uses this declaration.
- MonomialOrder.degreeproof · cited by 132
- MonomialOrder.degree_zeroproof · cited by 29
- MonomialOrder.withBotDegreeproof · cited by 26
- MonomialOrder.toWithBotSynproof · cited by 20
- MonomialOrder.leadingCoeff_zeroproof · cited by 14
- MonomialOrder.degree_monomialproof · cited by 12
- MonomialOrder.withBotDegree_eqproof · cited by 12
- MonomialOrder.le_degreestatement and proof · cited by 11
- MonomialOrder.degree_mul_lestatement and proof · cited by 10
- MonomialOrder.coeff_eq_zero_of_ltstatement and proof · cited by 6
- MonomialOrder.degree_add_of_ltstatement and proof · cited by 6
- MonomialOrder.degree_add_lestatement and proof · cited by 5