Documentation

Mathlib.Algebra.Order.Group.Multiset

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 #

theorem Multiset.mem_of_mem_nsmul {α : Type u_1} {a : α} {s : Multiset α} {n : } (h : a n s) :
a s
@[simp]
theorem Multiset.mem_nsmul {α : Type u_1} {a : α} {s : Multiset α} {n : } :
a n s n 0 a s
theorem Multiset.mem_nsmul_of_ne_zero {α : Type u_1} {a : α} {s : Multiset α} {n : } (h0 : n 0) :
a n s a s
theorem Multiset.nsmul_cons {α : Type u_1} {s : Multiset α} (n : ) (a : α) :
n (a ::ₘ s) = n {a} + n s

Cardinality #

Multiset.card bundled as a group hom.

Equations
    Instances For
      @[simp]
      theorem Multiset.cardHom_apply {α : Type u_1} (a✝ : Multiset α) :
      cardHom a✝ = a✝.card
      @[simp]
      theorem Multiset.card_nsmul {α : Type u_1} (s : Multiset α) (n : ) :
      (n s).card = n * s.card

      Multiset.replicate #

      Multiset.replicate as an AddMonoidHom.

      Equations
        Instances For
          @[simp]
          theorem Multiset.replicateAddMonoidHom_apply {α : Type u_1} (a : α) (n : ) :
          theorem Multiset.nsmul_replicate {α : Type u_1} {a : α} (n m : ) :
          n replicate m a = replicate (n * m) a
          theorem Multiset.nsmul_singleton {α : Type u_1} (a : α) (n : ) :
          n {a} = replicate n a

          Multiset.map #

          def Multiset.mapAddMonoidHom {α : Type u_1} {β : Type u_2} (f : αβ) :

          Multiset.map as an AddMonoidHom.

          Equations
            Instances For
              @[simp]
              theorem Multiset.mapAddMonoidHom_apply {α : Type u_1} {β : Type u_2} (f : αβ) (s : Multiset α) :
              @[simp]
              theorem Multiset.coe_mapAddMonoidHom {α : Type u_1} {β : Type u_2} (f : αβ) :
              theorem Multiset.map_nsmul {α : Type u_1} {β : Type u_2} (f : αβ) (n : ) (s : Multiset α) :
              map f (n s) = n map f s

              Subtraction #

              Multiset.filter #

              theorem Multiset.filter_nsmul {α : Type u_1} (p : αProp) [DecidablePred p] (s : Multiset α) (n : ) :
              filter p (n s) = n filter p s

              countP #

              @[simp]
              theorem Multiset.countP_nsmul {α : Type u_1} (p : αProp) [DecidablePred p] (s : Multiset α) (n : ) :
              countP p (n s) = n * countP p s
              def Multiset.countPAddMonoidHom {α : Type u_1} (p : αProp) [DecidablePred p] :

              countP p, the number of elements of a multiset satisfying p, promoted to an AddMonoidHom.

              Equations
                Instances For
                  @[simp]
                  theorem Multiset.coe_countPAddMonoidHom {α : Type u_1} (p : αProp) [DecidablePred p] :
                  @[simp]
                  theorem Multiset.dedup_nsmul {α : Type u_1} [DecidableEq α] {s : Multiset α} {n : } (hn : n 0) :
                  (n s).dedup = s.dedup
                  theorem Multiset.Nodup.le_nsmul_iff_le {α : Type u_1} {s t : Multiset α} {n : } (h : s.Nodup) (hn : n 0) :
                  s n t s t

                  Multiplicity of an element #

                  def Multiset.countAddMonoidHom {α : Type u_1} [DecidableEq α] (a : α) :

                  count a, the multiplicity of a in a multiset, promoted to an AddMonoidHom.

                  Equations
                    Instances For
                      @[simp]
                      theorem Multiset.coe_countAddMonoidHom {α : Type u_1} [DecidableEq α] (a : α) :
                      @[simp]
                      theorem Multiset.count_nsmul {α : Type u_1} [DecidableEq α] (a : α) (n : ) (s : Multiset α) :
                      count a (n s) = n * count a s
                      theorem Multiset.addHom_ext {α : Type u_1} {β : Type u_2} [AddZeroClass β] f g : Multiset α →+ β (h : ∀ (x : α), f {x} = g {x}) :
                      f = g
                      theorem Multiset.addHom_ext_iff {α : Type u_1} {β : Type u_2} [AddZeroClass β] {f g : Multiset α →+ β} :
                      f = g ∀ (x : α), f {x} = g {x}
                      theorem Multiset.le_smul_dedup {α : Type u_1} [DecidableEq α] (s : Multiset α) :
                      ∃ (n : ), s n s.dedup