Theorems · Definition · commutative algebra
Polynomial.freeMonic
(R : Type u_1) → [inst : CommRing R] → (n : ℕ) → Polynomial (MvPolynomial (Fin n) R)
The free monic polynomial of degree n, as a polynomial in R[X₁,...,Xₙ][X].
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 101 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- CommRingstatement and proof · cited by 17,173
- Polynomialstatement · cited by 5,681
- Finsuppstatement · cited by 5,255
- Finset.sumproof · cited by 5,195
- Finset.univproof · cited by 3,473
- MvPolynomialstatement · cited by 2,140
- Polynomial.Xproof · cited by 1,639
- Polynomial.Cproof · cited by 1,598
- MvPolynomial.Xproof · cited by 552
Cited by15
Results whose statement or proof uses this declaration.
- Polynomial.coeff_freeMonicstatement · cited by 6
- Polynomial.MonicDegreeEq.freeMonicproof · cited by 4
- Polynomial.monic_freeMonicstatement and proof · cited by 3
- Polynomial.natDegree_freeMonicstatement · cited by 3
- Polynomial.MonicDegreeEq.freeMonic_coestatement · cited by 2
- Polynomial.map_map_freeMonicstatement · cited by 1
- MvPolynomial.pderiv_inl_universalFactorizationMap_Xproof · cited by 1
- MvPolynomial.pderiv_inr_universalFactorizationMap_Xproof · cited by 1
- MvPolynomial.universalFactorizationMapPresentation_jacobiMatrixstatement and proof · cited by 1
- MvPolynomial.universalFactorizationMapPresentation_jacobianstatement and proof · cited by 1
- MvPolynomial.universalFactorizationMap_comp_mapproof · cited by 1
- MvPolynomial.universalFactorizationMap_freeMonicstatement and proof · cited by 1