Structures · Lean core
Std.Commutative
Commutative op says that op is a commutative operation,
i.e. a ∘ b = b ∘ a.
- Defined in
- Init.Core
- Shape
- One type argument · adds comm
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Forgetful instances
Every Std.Commutative is also a
Concrete types that are instances19
- Int
- Nat
- Rat
- Bool
- BitVec
- UInt64
- UInt8
- UInt16
- UInt32
- USize
- Int32
- Int8
- Int64
- Int16
- ISize
- Fin
- Set
- Finset
- Option
How is a type an instance?
Loading the hierarchy index…
Assumed by49
- Finset.fold
- Multiset.fold
- Multiset.fold_cons_left
- Finset.fold_insert
- Finset.fold_congr
- Multiset.fold_add
- Multiset.fold.congr_simp
- Finset.fold_cons
- Multiset.fold_zero
- Finset.fold_op_rel_iff_and
- Finset.fold_insert_idem
- Finset.fold_op_rel_iff_or
- Multiset.fold_dedup_idem
- Finset.fold_ite
- Finset.fold_empty
- Finset.fold_image_idem
- Multiset.fold_cons'_right
- Finset.fold_disjSum
- Multiset.coe_fold_r
- Finset.fold_singleton
- Finset.fold_disjUnion
- Finset.fold_union_inter
- Finset.fold.congr_simp
- Finset.fold_op_distrib
- List.Perm.foldr_op_eq
- Finset.fold_disjiUnion
- Finset.fold_image
- Finset.fold_map
- Multiset.fold_singleton
- Multiset.fold_cons_right
- Multiset.coe_fold_l
- Multiset.fold_bind
- Multiset.fold_hom
- Multiset.fold_eq_foldl
- Finset.fold_ite'
- Finset.fold_const
- Multiset.fold_distrib
- isSymmOp_of_isCommutative
- Multiset.fold_cons'_left
- Multiset.noncommFold_eq_fold
- Multiset.fold_eq_foldr
- Multiset.fold_union_inter
- Finset.fold_hom
- covariant_flip_iff
- List.foldl_eq_foldr
- instRightCommutativeOfCommutativeOfAssociative
- List.Perm.foldl_op_eq
- instLeftCommutativeOfCommutativeOfAssociative
- contravariant_flip_iff