Mathlib Map

Theorems · Definition · group theory

ShelfHom.toFun

{S₁ : Type u_1} → {S₂ : Type u_2} → [inst : Shelf S₁] → [inst_1 : Shelf S₂] → ShelfHom S₁ S₂ → S₁ → S₂

The function under the Shelf Homomorphism

Defined in
Mathlib.Algebra.Quandle
Cited by
4 results in Mathlib
Foundations
Depth 2 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.comp · cited by 3ShelfHom.compShelfHom.ext · cited by 1ShelfHom.extShelfHom.map_act' · cited by 1ShelfHom.map_act'ShelfHom.toFun_eq_coe · cited by 0ShelfHom.toFun_eq_coeShelfHom.ext_iff · cited by 0ShelfHom.ext_iffShelfHom · cited by 14ShelfHomShelf · cited by 10ShelfShelfHom.toFunCITED BYCITES

Cites2

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

  • ShelfHomstatement and proof · cited by 14
  • Shelfstatement and proof · cited by 10

Cited by5

Results whose statement or proof uses this declaration.