Mathlib Map

Theorems · Inductive type · group theory

ShelfHom

(S₁ : Type u_1) → (S₂ : Type u_2) → [Shelf S₁] → [Shelf S₂] → Type (max u_1 u_2)

The type of homomorphisms between shelves. This is also the notion of rack and quandle homomorphisms.

Defined in
Mathlib.Algebra.Quandle
Cited by
14 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Assumes
ShelfShelf
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

ShelfHom.toFun · cited by 4ShelfHom.toFunRack.toEnvelGroup · cited by 3Rack.toEnvelGroupShelfHom.comp · cited by 3ShelfHom.compQuandle.Conj.map · cited by 2Conj.mapRack.toEnvelGroup.map · cited by 2toEnvelGroup.mapRack.toEnvelGroup.mapAux · cited by 2toEnvelGroup.mapAuxShelfHom.mk.inj · cited by 1mk.injShelfHom.mk.noConfusion · cited by 1mk.noConfusionShelfHom.ext · cited by 1ShelfHom.extShelfHom.map_act' · cited by 1ShelfHom.map_act'ShelfHom.noConfusion · cited by 0ShelfHom.noConfusionShelfHom.noConfusionType · cited by 0ShelfHom.noConfusionTypeShelfHom.recOn · cited by 0ShelfHom.recOnShelfHom.toFun_eq_coe · cited by 0ShelfHom.toFun_eq_coeRack.envelAction_prop · cited by 0Rack.envelAction_propShelf · cited by 10ShelfShelfHomCITED BYCITES

Cites1

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

  • Shelfstatement · cited by 10

Cited by28

Results whose statement or proof uses this declaration.