Mathlib Map

Theorems · Theorem · group theory

Shelf.self_distrib

∀ {α : Type u} [self : Shelf α] {x y z : α}, Shelf.act x (Shelf.act y z) = Shelf.act (Shelf.act x y) (Shelf.act x z)

A verification that act is self-distributive

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

Around this declaration

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

Rack.self_act_act_eq · cited by 3Rack.self_act_act_eqUnitalShelf.act_self_act_eq · cited by 1UnitalShelf.act_self_act_…UnitalShelf.act_act_self_eq · cited by 1UnitalShelf.act_act_self_…UnitalShelf.assoc · cited by 0UnitalShelf.assocRack.self_distrib_inv · cited by 0Rack.self_distrib_invRack.ad_conj · cited by 0Rack.ad_conjRack.assoc_iff_id · cited by 0Rack.assoc_iff_idUnitalShelf.act_idem · cited by 0UnitalShelf.act_idemShelf.act · cited by 37Shelf.actShelf · cited by 10ShelfShelf.self_distribCITED BYCITES

Cites2

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

  • Shelf.actstatement · cited by 37
  • Shelfstatement and proof · cited by 10

Cited by8

Results whose statement or proof uses this declaration.