Documentation

instance Multiset.instAddLeftMono {α : Type u_1} :

AddLeftMono (Multiset α)

instance Multiset.instAddLeftReflectLE {α : Type u_1} :

AddLeftReflectLE (Multiset α)

@[implicit_reducible]

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.

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` #

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

ℕ →+ Multiset α

Multiset.replicate as an AddMonoidHom.

Instances For

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

Instances For

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

Instances For

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

Instances For

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