Theorems · Definition · ring theory
FreeRing.of
{α : Type u} → α → FreeRing αThe canonical map from α to FreeRing α.
- Defined in
- Mathlib.RingTheory.FreeRing
- Cited by
- 13 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.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- FreeMonoid.ofproof · cited by 69
- FreeAbelianGroup.ofproof · cited by 40
- FreeRingstatement · cited by 20
Cited by14
Results whose statement or proof uses this declaration.
- FreeRing.lift_ofstatement · cited by 2
- FreeRing.hom_extstatement and proof · cited by 1
- FreeRing.mapproof · cited by 1
- FreeRing.zero_ne_ofstatement · cited by 0
- FreeRing.coe_ofstatement · cited by 0
- FreeRing.coe_surjectiveproof · cited by 0
- FreeRing.hom_ext_iffstatement and proof · cited by 0
- FreeRing.induction_onstatement and proof · cited by 0
- FreeRing.lift_comp_ofstatement · cited by 0
- FreeRing.map_ofstatement and proof · cited by 0
- FreeRing.of_injectivestatement · cited by 0
- FreeRing.of_ne_onestatement · cited by 0