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 #

source
instance Multiset.instAddLeftMono {α : Type u_1} :
AddLeftMono (Multiset α)
source
instance Multiset.instAddLeftReflectLE {α : Type u_1} :
AddLeftReflectLE (Multiset α)
source
@[implicit_reducible]
instance Multiset.instAddCancelCommMonoid {α : Type u_1} :
AddCancelCommMonoid (Multiset α)
source
theorem Multiset.mem_of_mem_nsmul {α : Type u_1} {a : α} {s : Multiset α} {n : ℕ} (h : a ∈ n • s) :
a ∈ s
source
@[simp]
theorem Multiset.mem_nsmul {α : Type u_1} {a : α} {s : Multiset α} {n : ℕ} :
a ∈ n • s ↔ n ≠ 0 ∧ a ∈ s
source
theorem Multiset.mem_nsmul_of_ne_zero {α : Type u_1} {a : α} {s : Multiset α} {n : ℕ} (h0 : n ≠ 0) :
a ∈ n • s ↔ a ∈ s
source
theorem Multiset.nsmul_cons {α : Type u_1} {s : Multiset α} (n : ℕ) (a : α) :
n • (a ::ₘ s) = n • {a} + n • s

Cardinality #

source
def Multiset.cardHom {α : Type u_1} :
Multiset α →+ ℕ

Multiset.card bundled as a group hom.

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

    Multiset.replicate #

    source
    def Multiset.replicateAddMonoidHom {α : Type u_1} (a : α) :
    ℕ →+ Multiset α

    Multiset.replicate as an AddMonoidHom.

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

      Multiset.map #

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

      Multiset.map as an AddMonoidHom.

      Instances For
        source
        @[simp]
        theorem Multiset.mapAddMonoidHom_apply {α : Type u_1} {β : Type u_2} (f : α → β) (s : Multiset α) :
        (mapAddMonoidHom f) s = map f s
        source
        @[simp]
        theorem Multiset.coe_mapAddMonoidHom {α : Type u_1} {β : Type u_2} (f : α → β) :
        ⇑(mapAddMonoidHom f) = map f
        source
        theorem Multiset.map_nsmul {α : Type u_1} {β : Type u_2} (f : α → β) (n : ℕ) (s : Multiset α) :
        map f (n • s) = n • map f s

        Subtraction #

        source
        instance Multiset.instOrderedSub {α : Type u_1} [DecidableEq α] :
        OrderedSub (Multiset α)
        source
        instance Multiset.instExistsAddOfLE {α : Type u_1} :
        ExistsAddOfLE (Multiset α)

        Multiset.filter #

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

        countP #

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

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

        Instances For
          source
          @[simp]
          theorem Multiset.coe_countPAddMonoidHom {α : Type u_1} (p : α → Prop) [DecidablePred p] :
          ⇑(countPAddMonoidHom p) = countP p
          source
          @[simp]
          theorem Multiset.dedup_nsmul {α : Type u_1} [DecidableEq α] {s : Multiset α} {n : ℕ} (hn : n ≠ 0) :
          (n • s).dedup = s.dedup
          source
          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 #

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

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

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