Theorems · Definition · logic and foundations
FirstOrder.Field.genericMonicPoly
(n : ℕ) → FreeCommRing (Fin (n + 1))
A generic monic polynomial of degree n as an element of the
free commutative ring in n + 1 variables, with a variable for each
of the n non-leading coefficients of the polynomial and one variable (Fin.last n)
for X.
- Cited by
- 2 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.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finset.sumproof · cited by 5,195
- Finset.univproof · cited by 3,473
- FreeCommRingstatement · cited by 43
- FreeCommRing.ofproof · cited by 34
Cited by3
Results whose statement or proof uses this declaration.
- FirstOrder.Field.genericMonicPolyHasRootproof · cited by 4
- FirstOrder.Field.realize_genericMonicPolyHasRootproof · cited by 1
- FirstOrder.Field.lift_genericMonicPolystatement · cited by 1