Mathlib Map

Theorems · Definition · group theory

Shelf.act

{α : Type u} → [self : Shelf α] → α → α → α

The action of the Shelf over α

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

Around this declaration

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

Shelf.self_distrib · cited by 8Shelf.self_distribRack.act' · cited by 6Rack.act'Rack.left_cancel · cited by 6Rack.left_cancelRack.right_inv · cited by 6Rack.right_invRack.self_act_act_eq · cited by 3Rack.self_act_act_eqUnitalShelf.act_one · cited by 3UnitalShelf.act_oneRack.IsInvolutory · cited by 1Rack.IsInvolutoryRack.act_invAct_eq · cited by 1Rack.act_invAct_eqRack.left_inv · cited by 1Rack.left_invRack.self_act_eq_iff_eq · cited by 1Rack.self_act_eq_iff_eqRack.self_act_invAct_eq · cited by 1Rack.self_act_invAct_eqUnitalShelf.act_act_self_eq · cited by 1UnitalShelf.act_act_self_…UnitalShelf.act_self_act_eq · cited by 1UnitalShelf.act_self_act_…Rack.PreEnvelGroupRel'.casesOn · cited by 1PreEnvelGroupRel'.casesOnUnitalShelf.one_act · cited by 1UnitalShelf.one_actShelf · cited by 10ShelfShelf.actCITED BYCITES

Cites1

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

  • Shelfstatement and proof · cited by 10

Cited by67

Results whose statement or proof uses this declaration.