Theorems · Definition · logic and foundations
FirstOrder.Ring.genericPolyMap
{ι : Type u_1} → {κ : Type u_2} → (monoms : ι → Finset (κ →₀ ℕ)) → ι → FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ)Given a finite set of monomials monoms : ι → Finset (κ →₀ ℕ), the
genericPolyMap monoms is an indexed collection of elements of the FreeCommRing,
that can be evaluated to any collection p : ι → MvPolynomial κ R of
polynomials such that ∀ i, (p i).support ⊆ monoms i.
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 101 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- Finsuppstatement and proof · cited by 5,255
- Finset.sumproof · cited by 5,195
- Finsupp.prodproof · cited by 231
- Finset.attachproof · cited by 168
- FreeCommRingstatement · cited by 43
- FreeCommRing.ofproof · cited by 34
Cited by4
Results whose statement or proof uses this declaration.
- FirstOrder.genericPolyMapSurjOnOfInjOnproof · cited by 4
- FirstOrder.realize_genericPolyMapSurjOnOfInjOnproof · cited by 2
- FirstOrder.Ring.lift_genericPolyMapstatement · cited by 2
- FirstOrder.Ring.mvPolynomial_zeroLocus_definableproof · cited by 1