Mathlib.Algebra.Order.Group.Multiset

Multiset.instAddLeftMono instance

: AddLeftMono (Multiset α)

Full source

instance instAddLeftMono : AddLeftMono (Multiset α) where elim _s _t _u := Multiset.add_le_add_left

Left-Monotonicity of Addition on Multisets

Informal description

For any type $\alpha$, the collection of multisets over $\alpha$ is equipped with a left-monotone addition operation. This means that for any multisets $s$, $t$, and $u$ over $\alpha$, if $s \leq t$, then $u + s \leq u + t$.

Multiset.instAddLeftReflectLE instance

: AddLeftReflectLE (Multiset α)

Full source

instance instAddLeftReflectLE : AddLeftReflectLE (Multiset α) where
  elim _s _t _u := Multiset.le_of_add_le_add_left

Order Reflection under Left Addition in Multisets

Informal description

For any type $\alpha$, the collection of multisets over $\alpha$ reflects the order relation under left addition. That is, for any multisets $s$, $t$, and $u$ over $\alpha$, if $u + s \leq u + t$, then $s \leq t$.

Multiset.instAddCancelCommMonoid instance

: AddCancelCommMonoid (Multiset α)

Full source

instance instAddCancelCommMonoid : AddCancelCommMonoid (Multiset α) where
  add_comm := Multiset.add_comm
  add_assoc := Multiset.add_assoc
  zero_add := Multiset.zero_add
  add_zero := Multiset.add_zero
  add_left_cancel _ _ _ := Multiset.add_right_inj.1
  nsmul := nsmulRec

Multisets Form an Additive Commutative Monoid with Cancellation

Informal description

For any type $\alpha$, the collection of multisets over $\alpha$ forms an additive commutative monoid with cancellation. This means that for any multisets $s$, $t$, and $u$ over $\alpha$, the following properties hold: 1. Commutativity: $s + t = t + s$ 2. Associativity: $(s + t) + u = s + (t + u)$ 3. Identity: $s + 0 = s$ and $0 + s = s$ 4. Cancellation: If $s + t = s + u$, then $t = u$

Multiset.mem_of_mem_nsmul theorem

{a : α} {s : Multiset α} {n : ℕ} (h : a ∈ n • s) : a ∈ s

Full source

lemma mem_of_mem_nsmul {a : α} {s : Multiset α} {n : ℕ} (h : a ∈ n • s) : a ∈ s := by
  induction' n with n ih
  · rw [zero_nsmul] at h
    exact absurd h (not_mem_zero _)
  · rw [succ_nsmul, mem_add] at h
    exact h.elim ih id

Membership in Scalar Multiple Implies Membership in Original Multiset: $a \in n \cdot s \Rightarrow a \in s$

Informal description

For any element $a$ of type $\alpha$, multiset $s$ over $\alpha$, and natural number $n$, if $a$ belongs to the scalar multiple $n \cdot s$, then $a$ belongs to $s$.

Multiset.mem_nsmul theorem

{a : α} {s : Multiset α} {n : ℕ} : a ∈ n • s ↔ n ≠ 0 ∧ a ∈ s

Full source

@[simp]
lemma mem_nsmul {a : α} {s : Multiset α} {n : ℕ} : a ∈ n • sa ∈ n • s ↔ n ≠ 0 ∧ a ∈ s := by
  refine ⟨fun ha ↦ ⟨?_, mem_of_mem_nsmul ha⟩, fun h ↦ ?_⟩
  · rintro rfl
    simp [zero_nsmul] at ha
  obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero h.1
  rw [succ_nsmul, mem_add]
  exact Or.inr h.2

Membership in Scalar Multiple of Multiset: $a \in n \cdot s \leftrightarrow n \neq 0 \land a \in s$

Informal description

For any element $a$ of type $\alpha$, multiset $s$ over $\alpha$, and natural number $n$, the element $a$ belongs to the scalar multiple $n \cdot s$ if and only if $n$ is nonzero and $a$ belongs to $s$.

Multiset.mem_nsmul_of_ne_zero theorem

{a : α} {s : Multiset α} {n : ℕ} (h0 : n ≠ 0) : a ∈ n • s ↔ a ∈ s

Full source

lemma mem_nsmul_of_ne_zero {a : α} {s : Multiset α} {n : ℕ} (h0 : n ≠ 0) : a ∈ n • sa ∈ n • s ↔ a ∈ s := by
  simp [*]

Membership in Scalar Multiple of Multiset for Nonzero Scalar: $a \in n \cdot s \leftrightarrow a \in s$ when $n \neq 0$

Informal description

For any element $a$ of type $\alpha$, multiset $s$ over $\alpha$, and nonzero natural number $n$, the element $a$ belongs to the scalar multiple $n \cdot s$ if and only if $a$ belongs to $s$.

Multiset.nsmul_cons theorem

{s : Multiset α} (n : ℕ) (a : α) : n • (a ::ₘ s) = n • ({ a } : Multiset α) + n • s

Full source

lemma nsmul_cons {s : Multiset α} (n : ℕ) (a : α) :
    n • (a ::ₘ s) = n • ({a} : Multiset α) + n • s := by
  rw [← singleton_add, nsmul_add]

Distributivity of Scalar Multiplication over Multiset Insertion: $n \cdot (a \mathbin{::} s) = n \cdot \{a\} + n \cdot s$

Informal description

For any natural number $n$, element $a$ of type $\alpha$, and multiset $s$ over $\alpha$, the scalar multiplication of $n$ with the multiset obtained by inserting $a$ into $s$ is equal to the sum of the scalar multiplication of $n$ with the singleton multiset $\{a\}$ and the scalar multiplication of $n$ with $s$. That is, $n \cdot (a \mathbin{::} s) = n \cdot \{a\} + n \cdot s$.

Multiset.cardHom definition

: Multiset α →+ ℕ

Full source

/-- `Multiset.card` bundled as a group hom. -/
@[simps]
def cardHom : MultisetMultiset α →+ ℕ where
  toFun := card
  map_zero' := card_zero
  map_add' := card_add

Cardinality homomorphism for multisets

Informal description

The bundled group homomorphism version of the cardinality function for multisets, which maps a multiset $s$ over a type $\alpha$ to its cardinality $|s|$ as a natural number. This homomorphism preserves the additive structure, satisfying: 1. $f(0) = 0$ (the empty multiset maps to zero) 2. $f(s + t) = f(s) + f(t)$ for any multisets $s, t$ (cardinality is additive under multiset sum)

Multiset.card_nsmul theorem

(s : Multiset α) (n : ℕ) : card (n • s) = n * card s

Full source

@[simp]
lemma card_nsmul (s : Multiset α) (n : ℕ) : card (n • s) = n * card s := cardHom.map_nsmul ..

Cardinality of Scalar Multiple of a Multiset: $|n \cdot s| = n \cdot |s|$

Informal description

For any multiset $s$ over a type $\alpha$ and any natural number $n$, the cardinality of the scalar multiple $n \cdot s$ is equal to $n$ times the cardinality of $s$, i.e., $|n \cdot s| = n \cdot |s|$.

Multiset.replicateAddMonoidHom definition

(a : α) : ℕ →+ Multiset α

Full source

/-- `Multiset.replicate` as an `AddMonoidHom`. -/
@[simps]
def replicateAddMonoidHom (a : α) : ℕℕ →+ Multiset α where
  toFun n := replicate n a
  map_zero' := replicate_zero a
  map_add' _ _ := replicate_add _ _ a

Replication as an additive monoid homomorphism

Informal description

For a given element $a$ of type $\alpha$, the function `Multiset.replicateAddMonoidHom` is an additive monoid homomorphism from the natural numbers $\mathbb{N}$ to the additive monoid of multisets over $\alpha$. It maps each natural number $n$ to the multiset consisting of $n$ copies of $a$. More precisely, this homomorphism satisfies: 1. $f(0) = \emptyset$ (the empty multiset) 2. $f(n + m) = f(n) + f(m)$ for all $n, m \in \mathbb{N}$

Multiset.nsmul_replicate theorem

{a : α} (n m : ℕ) : n • replicate m a = replicate (n * m) a

Full source

lemma nsmul_replicate {a : α} (n m : ℕ) : n • replicate m a = replicate (n * m) a :=
  ((replicateAddMonoidHom a).map_nsmul _ _).symm

Scalar Multiplication of Replicated Multiset: $n \cdot \{a, \dots, a\} = \{a, \dots, a\}$ ($n \times m$ times)

Informal description

For any element $a$ of type $\alpha$ and natural numbers $n, m \in \mathbb{N}$, the scalar multiplication of $n$ with the multiset consisting of $m$ copies of $a$ equals the multiset consisting of $n \times m$ copies of $a$. In symbols: $$ n \cdot \{a, \dots, a\} = \{a, \dots, a\} $$ where the left multiset has $m$ copies of $a$ and the right multiset has $n \times m$ copies.

Multiset.nsmul_singleton theorem

(a : α) (n) : n • ({ a } : Multiset α) = replicate n a

Full source

lemma nsmul_singleton (a : α) (n) : n • ({a} : Multiset α) = replicate n a := by
  rw [← replicate_one, nsmul_replicate, mul_one]

Scalar Multiplication of Singleton Multiset: $n \cdot \{a\} = \{a, \dots, a\}$ ($n$ times)

Informal description

For any element $a$ of type $\alpha$ and any natural number $n$, the scalar multiplication of $n$ with the singleton multiset $\{a\}$ equals the multiset consisting of $n$ copies of $a$. In symbols: $$ n \cdot \{a\} = \{a, \dots, a\} $$ where the right multiset has $n$ copies of $a$.

Multiset.mapAddMonoidHom definition

(f : α → β) : Multiset α →+ Multiset β

Full source

/-- `Multiset.map` as an `AddMonoidHom`. -/
@[simps]
def mapAddMonoidHom (f : α → β) : MultisetMultiset α →+ Multiset β where
  toFun := map f
  map_zero' := map_zero _
  map_add' := map_add _

Additive monoid homomorphism induced by a function on multisets

Informal description

For any function $ f : \alpha \to \beta $, the map $ \text{mapAddMonoidHom} \, f $ is an additive monoid homomorphism from the additive monoid of multisets over $ \alpha $ to the additive monoid of multisets over $ \beta $. It satisfies: 1. $ \text{mapAddMonoidHom} \, f \, 0 = 0 $ (preservation of zero) 2. $ \text{mapAddMonoidHom} \, f (s + t) = \text{mapAddMonoidHom} \, f \, s + \text{mapAddMonoidHom} \, f \, t $ for all multisets $ s, t $ over $ \alpha $ (preservation of addition)

Multiset.coe_mapAddMonoidHom theorem

(f : α → β) : (mapAddMonoidHom f : Multiset α → Multiset β) = map f

Full source

@[simp]
lemma coe_mapAddMonoidHom (f : α → β) : (mapAddMonoidHom f : Multiset α → Multiset β) = map f := rfl

Coincidence of Map Monoid Homomorphism and Map Operation on Multisets

Informal description

For any function $f : \alpha \to \beta$, the additive monoid homomorphism $\text{mapAddMonoidHom}\, f$ from the additive monoid of multisets over $\alpha$ to the additive monoid of multisets over $\beta$ coincides with the map operation $\text{map}\, f$ on multisets. That is, $\text{mapAddMonoidHom}\, f = \text{map}\, f$.

Multiset.map_nsmul theorem

(f : α → β) (n : ℕ) (s) : map f (n • s) = n • map f s

Full source

lemma map_nsmul (f : α → β) (n : ℕ) (s) : map f (n • s) = n • map f s :=
  (mapAddMonoidHom f).map_nsmul _ _

Multiset map preserves scalar multiplication: $\text{map}\, f (n \cdot s) = n \cdot \text{map}\, f (s)$

Informal description

For any function $f : \alpha \to \beta$, any natural number $n$, and any multiset $s$ over $\alpha$, the image of the $n$-fold sum of $s$ under $f$ is equal to the $n$-fold sum of the image of $s$ under $f$. In symbols: \[ \text{map}\, f (n \cdot s) = n \cdot \text{map}\, f (s) \]

Multiset.instOrderedSub instance

: OrderedSub (Multiset α)

Full source

instance : OrderedSub (Multiset α) where tsub_le_iff_right _n _m _k := Multiset.sub_le_iff_le_add

Ordered Subtraction Structure on Multisets

Informal description

For any type $\alpha$, the collection of multisets over $\alpha$ forms an ordered subtraction structure. This means that for any multisets $s, t, u$, the inequality $s - t \leq u$ holds if and only if $s \leq u + t$.

Multiset.instExistsAddOfLE instance

: ExistsAddOfLE (Multiset α)

Full source

instance : ExistsAddOfLE (Multiset α) where
  exists_add_of_le h := leInductionOn h fun s ↦
      let ⟨l, p⟩ := s.exists_perm_append; ⟨l, Quot.sound p⟩

Existence of Additive Difference for Multisets

Informal description

For any type $\alpha$, the collection of multisets over $\alpha$ satisfies the property that for any two multisets $s$ and $t$, if $s \leq t$ then there exists a multiset $u$ such that $t = s + u$.

Multiset.filter_nsmul theorem

(s : Multiset α) (n : ℕ) : filter p (n • s) = n • filter p s

Full source

lemma filter_nsmul (s : Multiset α) (n : ℕ) : filter p (n • s) = n • filter p s := by
  refine s.induction_on ?_ ?_
  · simp only [filter_zero, nsmul_zero]
  · intro a ha ih
    rw [nsmul_cons, filter_add, ih, filter_cons, nsmul_add]
    congr
    split_ifs with hp <;>
      · simp only [filter_eq_self, nsmul_zero, filter_eq_nil]
        intro b hb
        rwa [mem_singleton.mp (mem_of_mem_nsmul hb)]

Filter Commutes with Scalar Multiplication: $\text{filter } p (n \cdot s) = n \cdot \text{filter } p s$

Informal description

For any multiset $s$ over a type $\alpha$, any predicate $p$ on $\alpha$, and any natural number $n$, the filter of the scalar multiple $n \cdot s$ under $p$ is equal to the scalar multiple $n \cdot \text{filter } p s$. That is, \[ \text{filter } p (n \cdot s) = n \cdot \text{filter } p s. \]

Multiset.countP_nsmul theorem

(s) (n : ℕ) : countP p (n • s) = n * countP p s

Full source

@[simp]
lemma countP_nsmul (s) (n : ℕ) : countP p (n • s) = n * countP p s := by
  induction n <;> simp [*, succ_nsmul, succ_mul, zero_nsmul]

Linear Scaling of Count under Multiset Scaling: $\text{countP}_p(n \cdot s) = n \cdot \text{countP}_p(s)$

Informal description

For any multiset $s$ over a type $\alpha$, any predicate $p$ on $\alpha$, and any natural number $n$, the count of elements (with multiplicity) in $s$ satisfying $p$ scales linearly with $n$ when the multiset is scaled by $n$. That is, \[ \text{countP}_p(n \cdot s) = n \cdot \text{countP}_p(s). \]

Multiset.countPAddMonoidHom definition

: Multiset α →+ ℕ

Full source

/-- `countP p`, the number of elements of a multiset satisfying `p`, promoted to an
`AddMonoidHom`. -/
def countPAddMonoidHom : MultisetMultiset α →+ ℕ where
  toFun := countP p
  map_zero' := countP_zero _
  map_add' := countP_add _

Count predicate as an additive monoid homomorphism

Informal description

The function that maps a multiset $s$ over a type $\alpha$ to the count of elements (with multiplicity) in $s$ that satisfy a predicate $p$, promoted to an additive monoid homomorphism from multisets to natural numbers. This means it satisfies: 1. $\text{countP}_p(0) = 0$ (preservation of zero) 2. $\text{countP}_p(s + t) = \text{countP}_p(s) + \text{countP}_p(t)$ for all multisets $s, t$ (additivity)

Multiset.coe_countPAddMonoidHom theorem

: (countPAddMonoidHom p : Multiset α → ℕ) = countP p

Full source

@[simp] lemma coe_countPAddMonoidHom : (countPAddMonoidHom p : Multiset α → ℕ) = countP p := rfl

Count Predicate Homomorphism Coincides with Count Function: $\text{countPAddMonoidHom}_p = \text{countP}_p$

Informal description

The additive monoid homomorphism $\text{countP}_p$ from multisets over $\alpha$ to natural numbers, which counts elements (with multiplicity) satisfying a predicate $p$, is equal to the function $\text{countP}_p$ when viewed as a plain function.

Multiset.dedup_nsmul theorem

[DecidableEq α] {s : Multiset α} {n : ℕ} (hn : n ≠ 0) : (n • s).dedup = s.dedup

Full source

@[simp] lemma dedup_nsmul [DecidableEq α] {s : Multiset α} {n : ℕ} (hn : n ≠ 0) :
    (n • s).dedup = s.dedup := by ext a; by_cases h : a ∈ s <;> simp [h, hn]

Deduplication of Scalar Multiple: $\text{dedup}(n \cdot s) = \text{dedup}(s)$ for $n \neq 0$

Informal description

For any multiset $s$ over a type $\alpha$ with decidable equality and any nonzero natural number $n$, the deduplication of the $n$-fold sum of $s$ is equal to the deduplication of $s$. That is, $\text{dedup}(n \cdot s) = \text{dedup}(s)$ for $n \neq 0$.

Multiset.Nodup.le_nsmul_iff_le theorem

{s t : Multiset α} {n : ℕ} (h : s.Nodup) (hn : n ≠ 0) : s ≤ n • t ↔ s ≤ t

Full source

lemma Nodup.le_nsmul_iff_le {s t : Multiset α} {n : ℕ} (h : s.Nodup) (hn : n ≠ 0) :
    s ≤ n • t ↔ s ≤ t := by
  classical simp [← h.le_dedup_iff_le, Iff.comm, ← h.le_dedup_iff_le, hn]

Submultiset Relation Preserved Under Scalar Multiplication for Nodup Multisets: $s \leq n \cdot t \leftrightarrow s \leq t$ ($n \neq 0$)

Informal description

For any multisets $s$ and $t$ over a type $\alpha$, if $s$ has no duplicates ($s.\text{Nodup}$) and $n$ is a nonzero natural number ($n \neq 0$), then $s$ is a submultiset of the $n$-fold sum of $t$ if and only if $s$ is a submultiset of $t$. In other words, $s \leq n \cdot t \leftrightarrow s \leq t$.

Multiset.countAddMonoidHom definition

(a : α) : Multiset α →+ ℕ

Full source

/-- `count a`, the multiplicity of `a` in a multiset, promoted to an `AddMonoidHom`. -/
def countAddMonoidHom (a : α) : MultisetMultiset α →+ ℕ :=
  countPAddMonoidHom (a = ·)

Multiplicity count as an additive monoid homomorphism

Informal description

For any element $a$ of type $\alpha$, the function that maps a multiset $s$ to the multiplicity of $a$ in $s$ (counted with multiplicity), promoted to an additive monoid homomorphism from multisets to natural numbers. This means it satisfies: 1. $\text{count}_a(0) = 0$ (preservation of the empty multiset) 2. $\text{count}_a(s + t) = \text{count}_a(s) + \text{count}_a(t)$ for all multisets $s, t$ (additivity)

Multiset.coe_countAddMonoidHom theorem

(a : α) : (countAddMonoidHom a : Multiset α → ℕ) = count a

Full source

@[simp]
lemma coe_countAddMonoidHom (a : α) : (countAddMonoidHom a : Multiset α → ℕ) = count a := rfl

Equivalence of Count Homomorphism and Multiplicity Function on Multisets

Informal description

For any element $a$ of type $\alpha$, the additive monoid homomorphism $\mathrm{count}_a$ from multisets over $\alpha$ to natural numbers coincides with the multiplicity function $\mathrm{count}(a, \cdot)$, i.e., \[ \mathrm{count}_a(s) = \mathrm{count}(a, s) \] for any multiset $s$ over $\alpha$.

Multiset.count_nsmul theorem

(a : α) (n s) : count a (n • s) = n * count a s

Full source

@[simp]
lemma count_nsmul (a : α) (n s) : count a (n • s) = n * count a s := by
  induction n <;> simp [*, succ_nsmul, succ_mul, zero_nsmul]

Multiplicity in Scalar Multiple of a Multiset: $\mathrm{count}(a, n \cdot s) = n \cdot \mathrm{count}(a, s)$

Informal description

For any element $a$ of type $\alpha$, natural number $n$, and multiset $s$ over $\alpha$, the multiplicity of $a$ in the scalar multiple $n \cdot s$ is equal to $n$ times the multiplicity of $a$ in $s$, i.e., \[ \mathrm{count}(a, n \cdot s) = n \cdot \mathrm{count}(a, s). \]

Multiset.addHom_ext theorem

[AddZeroClass β] ⦃f g : Multiset α →+ β⦄ (h : ∀ x, f { x } = g { x }) : f = g

Full source

@[ext]
lemma addHom_ext [AddZeroClass β] ⦃f g : MultisetMultiset α →+ β⦄ (h : ∀ x, f {x} = g {x}) : f = g := by
  ext s
  induction' s using Multiset.induction_on with a s ih
  · simp only [_root_.map_zero]
  · simp only [← singleton_add, _root_.map_add, ih, h]

Uniqueness of Additive Monoid Homomorphisms from Multisets via Singleton Condition

Informal description

Let $β$ be an additive monoid (i.e., a type with a zero element and addition operation). For any two additive monoid homomorphisms $f, g$ from the multiset monoid over type $α$ to $β$, if $f$ and $g$ agree on all singleton multisets $\{x\}$ (i.e., $f(\{x\}) = g(\{x\})$ for all $x \in α$), then $f = g$.

Multiset.le_smul_dedup theorem

[DecidableEq α] (s : Multiset α) : ∃ n : ℕ, s ≤ n • dedup s

Full source

theorem le_smul_dedup [DecidableEq α] (s : Multiset α) : ∃ n : ℕ, s ≤ n • dedup s :=
  ⟨(s.map fun a => count a s).fold max 0,
    le_iff_count.2 fun a => by
      rw [count_nsmul]; by_cases h : a ∈ s
      · refine le_trans ?_ (Nat.mul_le_mul_left _ <| count_pos.2 <| mem_dedup.2 h)
        have : count a s ≤ fold max 0 (map (fun a => count a s) (a ::ₘ erase s a)) := by
          simp [le_max_left]
        rw [cons_erase h] at this
        simpa [mul_succ] using this
      · simp [count_eq_zero.2 h, Nat.zero_le]⟩

Existence of Scalar Multiple Containing Multiset via Deduplication: $s \leq n \cdot \mathrm{dedup}(s)$

Informal description

For any multiset $s$ over a type $\alpha$ with decidable equality, there exists a natural number $n$ such that $s$ is contained in the scalar multiple $n \cdot \mathrm{dedup}(s)$, where $\mathrm{dedup}(s)$ is the deduplicated version of $s$ (i.e., $s \leq n \cdot \mathrm{dedup}(s)$).