Multisets form an ordered monoid #
This file contains the ordered monoid instance on multisets, and lemmas related to it.
See note [foundational algebra order theory].
Additive monoid #
Equations
Cardinality #
@[simp]
@[simp]
@[simp]
Subtraction #
countP #
countP p
, the number of elements of a multiset satisfying p
, promoted to an
AddMonoidHom
.
Equations
Instances For
@[simp]
Multiplicity of an element #
@[simp]