Theorems · Definition · group theory
Rack.toEnvelGroup
(R : Type u_1) → [inst : Rack R] → ShelfHom R (Quandle.Conj (Rack.EnvelGroup R))
The canonical homomorphism from a rack to its enveloping group.
Satisfies universal properties given by toEnvelGroup.map and toEnvelGroup.univ.
- Defined in
- Mathlib.Algebra.Quandle
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 27 from the axioms · uses propext, Quot.sound
- Assumes
- Rack
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.
- Rackstatement and proof · cited by 49
- ShelfHomstatement · cited by 14
- Quandle.Conjstatement · cited by 7
- Rack.EnvelGroupstatement · cited by 3
Cited by4
Results whose statement or proof uses this declaration.
- Rack.toEnvelGroup.mapproof · cited by 2
- Rack.envelAction_propstatement · cited by 0
- Rack.toEnvelGroup.univstatement · cited by 0
- Rack.toEnvelGroup.univ_uniqstatement and proof · cited by 0