Structures · Logic and sets
LeftCommutative
LeftCommutative op where op : α → β → β says that op is a left-commutative operation,
i.e. op a₁ (op a₂ b) = op a₂ (op a₁ b).
- Defined in
- Mathlib.Logic.OpClass
- Shape
- One type argument · adds left_comm
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by18
- Multiset.foldr
- Multiset.foldr_cons
- Multiset.foldr_swap
- LeftCommutative.left_comm
- List.foldr_cons_eq_foldr_apply
- Multiset.coe_foldr_swap
- Multiset.foldr_induction'
- Multiset.foldr_induction
- List.Perm.foldr_eq
- Multiset.foldr.congr_simp
- Multiset.foldr_singleton
- instRightCommutativeOfLeftCommutative
- Multiset.foldr_zero
- Multiset.noncommFoldr_eq_foldr
- Multiset.foldr_add
- Multiset.coe_foldr
- List.foldr_eq_of_comm'
- List.foldl_flip_eq_foldr