Structures · Logic and sets
RightCommutative
RightCommutative op where op : β → α → β says that op is a right-commutative operation,
i.e. op (op b a₁) a₂ = op (op b a₂) a₁.
- Defined in
- Mathlib.Logic.OpClass
- Shape
- One type argument · adds right_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.foldl
- List.foldl_cons_eq_apply_foldl
- RightCommutative.right_comm
- Multiset.foldl_cons
- List.Perm.foldl_eq
- List.foldr_flip_eq_foldl
- Multiset.foldl.congr_simp
- Multiset.foldl_induction'
- Multiset.foldl_swap
- Multiset.foldl_induction
- Multiset.foldl_add
- List.foldl_eq_of_comm'
- List.foldl_eq_of_comm_of_assoc
- Multiset.foldl_zero
- Multiset.coe_foldl
- List.foldl_eq_foldr'
- instLeftCommutativeOfRightCommutative
- List.foldl_assoc_comm_cons