Mathlib Map

Theorems · Definition · group theory

Rack.EnvelGroup

(R : Type u_1) → [Rack R] → Type u_1

The universal enveloping group for the rack R.

Defined in
Mathlib.Algebra.Quandle
Cited by
3 results in Mathlib
Foundations
Depth 9 from the axioms · uses no axioms
Assumes
Rack
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Rack.toEnvelGroup · cited by 3Rack.toEnvelGroupRack.toEnvelGroup.map · cited by 2toEnvelGroup.mapRack.envelAction · cited by 1Rack.envelActionRack.toEnvelGroup.univ · cited by 0toEnvelGroup.univRack.toEnvelGroup.univ_uniq · cited by 0toEnvelGroup.univ_uniqRack.envelAction_prop · cited by 0Rack.envelAction_propRack · cited by 49RackRack.EnvelGroupCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Rackstatement and proof · cited by 49

Cited by6

Results whose statement or proof uses this declaration.