Theorems · Definition · commutative algebra
FreeCommRing.of
{α : Type u} → α → FreeCommRing αThe canonical map from α to the free commutative ring on α.
- Defined in
- Mathlib.RingTheory.FreeCommRing
- Cited by
- 34 results in Mathlib
- Foundations
- Depth 79 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.
- DFunLike.coeproof · cited by 62,936
- Multiplicative.ofAddproof · cited by 237
- FreeCommRingstatement · cited by 43
- FreeAbelianGroup.ofproof · cited by 40
Cited by44
Results whose statement or proof uses this declaration.
- Ring.DirectLimitproof · cited by 26
- Ring.DirectLimit.ofproof · cited by 21
- FreeCommRing.IsSupportedproof · cited by 12
- FreeCommRing.lift_ofstatement · cited by 9
- Ring.DirectLimit.liftproof · cited by 6
- FirstOrder.Ring.realize_termOfFreeCommRingproof · cited by 5
- Ring.DirectLimit.hom_extproof · cited by 5
- FreeCommRing.induction_onstatement and proof · cited by 4
- FreeCommRing.hom_extstatement and proof · cited by 3
- FirstOrder.Ring.genericPolyMapproof · cited by 3
- FreeRing.toFreeCommRingproof · cited by 2
- Ring.DirectLimit.exists_ofproof · cited by 2