Mathlib Map

Theorems · Definition · group theory

ShelfHom.id

(S : Type u_4) → [inst : Shelf S] → ShelfHom S S

The identity homomorphism

Defined in
Mathlib.Algebra.Quandle
Cited by
0 results in Mathlib
Foundations
Depth 7 from the axioms · uses propext, Quot.sound
Assumes
Shelf

Around this declaration

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

Cites2

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

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

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.