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

instance Multiset.instAddLeftMono {α : Type u_1} : AddLeftMono (Multiset α)

instance Multiset.instAddLeftReflectLE {α : Type u_1} : AddLeftReflectLE (Multiset α)

instance Multiset.instAddCancelCommMonoid {α : Type u_1} : AddCancelCommMonoid (Multiset α)

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

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

Multiset.card bundled as a group hom.

@[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

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

Multiset.replicate as an AddMonoidHom.

@[simp]

theorem Multiset.replicateAddMonoidHom_apply {α : Type u_1} (a : α) (n : ℕ) : (replicateAddMonoidHom a) n = replicate n a

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 α →+ Multiset β

Multiset.map as an AddMonoidHom.

@[simp]

theorem Multiset.mapAddMonoidHom_apply {α : Type u_1} {β : Type u_2} (f : α → β) (s : Multiset α) : (mapAddMonoidHom f) s = map f s

@[simp]

theorem Multiset.coe_mapAddMonoidHom {α : Type u_1} {β : Type u_2} (f : α → β) : ⇑(mapAddMonoidHom f) = map f

theorem Multiset.map_nsmul {α : Type u_1} {β : Type u_2} (f : α → β) (n : ℕ) (s : Multiset α) : map f (n • s) = n • map f s

Subtraction

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

instance Multiset.instExistsAddOfLE {α : Type u_1} : ExistsAddOfLE (Multiset α)

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] : Multiset α →+ ℕ

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

@[simp]

theorem Multiset.coe_countPAddMonoidHom {α : Type u_1} (p : α → Prop) [DecidablePred p] : ⇑(countPAddMonoidHom p) = countP 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 : α) : Multiset α →+ ℕ

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

@[simp]

theorem Multiset.coe_countAddMonoidHom {α : Type u_1} [DecidableEq α] (a : α) : ⇑(countAddMonoidHom a) = count 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