Theorems · Theorem · group theory
Rack.left_cancel
∀ {R : Type u_1} [inst : Rack R] (x : R) {y y' : R}, Shelf.act x y = Shelf.act x y' ↔ y = y'- Defined in
- Mathlib.Algebra.Quandle
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses Quot.sound
- Assumes
- Rack
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Equiv.injectiveproof · cited by 464
- Rackstatement and proof · cited by 49
- Shelf.actstatement and proof · cited by 37
- Rack.act'proof · cited by 6
Cited by6
Results whose statement or proof uses this declaration.
- Rack.self_act_eq_iff_eqproof · cited by 1
- Rack.self_act_invAct_eqproof · cited by 1
- Rack.self_distrib_invproof · cited by 0
- Rack.assoc_iff_idproof · cited by 0
- Quandle.fix_invproof · cited by 0
- Rack.involutory_invAct_eq_actproof · cited by 0