# Repeating elements in multisets #

## Main definitions #

- `replicate n a` is the multiset containing only `a` with multiplicity `n`

### `Multiset.replicate` #

source
def Multiset.replicate {α : Type u_1} (n : ℕ) (a : α) :
Multiset α

`replicate n a` is the multiset containing only `a` with multiplicity `n`.

Equations

- Multiset.replicate n a = ↑(List.replicate n a)

Instances For

source
theorem Multiset.coe_replicate {α : Type u_1} (n : ℕ) (a : α) :
↑(List.replicate n a) = replicate n a
source
@[simp]
theorem Multiset.replicate_zero {α : Type u_1} (a : α) :
replicate 0 a = 0
source
@[simp]
theorem Multiset.replicate_succ {α : Type u_1} (a : α) (n : ℕ) :
replicate (n + 1) a = a ::ₘ replicate n a
source
theorem Multiset.replicate_add {α : Type u_1} (m n : ℕ) (a : α) :
replicate (m + n) a = replicate m a + replicate n a
source
theorem Multiset.replicate_one {α : Type u_1} (a : α) :
replicate 1 a = {a}
source
@[simp]
theorem Multiset.card_replicate {α : Type u_1} (n : ℕ) (a : α) :
(replicate n a).card = n
source
theorem Multiset.mem_replicate {α : Type u_1} {a b : α} {n : ℕ} :
b ∈ replicate n a ↔ n ≠ 0 ∧ b = a
source
theorem Multiset.eq_of_mem_replicate {α : Type u_1} {a b : α} {n : ℕ} :
b ∈ replicate n a → b = a
source
theorem Multiset.eq_replicate_card {α : Type u_1} {a : α} {s : Multiset α} :
s = replicate s.card a ↔ ∀ (b : α), b ∈ s → b = a
source
theorem Multiset.eq_replicate_of_mem {α : Type u_1} {a : α} {s : Multiset α} :
(∀ (b : α), b ∈ s → b = a) → s = replicate s.card a

Alias of the reverse direction of `Multiset.eq_replicate_card`.

source
theorem Multiset.eq_replicate {α : Type u_1} {a : α} {n : ℕ} {s : Multiset α} :
s = replicate n a ↔ s.card = n ∧ ∀ (b : α), b ∈ s → b = a
source
theorem Multiset.replicate_right_injective {α : Type u_1} {n : ℕ} (hn : n ≠ 0) :
Function.Injective (replicate n)
source
@[simp]
theorem Multiset.replicate_right_inj {α : Type u_1} {a b : α} {n : ℕ} (h : n ≠ 0) :
replicate n a = replicate n b ↔ a = b
source
theorem Multiset.replicate_left_injective {α : Type u_1} (a : α) :
Function.Injective fun (x : ℕ) => replicate x a
source
theorem Multiset.replicate_subset_singleton {α : Type u_1} (n : ℕ) (a : α) :
replicate n a ⊆ {a}
source
theorem Multiset.replicate_le_coe {α : Type u_1} {a : α} {n : ℕ} {l : List α} :
replicate n a ≤ ↑l ↔ (List.replicate n a).Sublist l
source
theorem Multiset.replicate_le_replicate {α : Type u_1} (a : α) {k n : ℕ} :
replicate k a ≤ replicate n a ↔ k ≤ n
source
theorem Multiset.replicate_mono {α : Type u_1} (a : α) {k n : ℕ} (h : k ≤ n) :
replicate k a ≤ replicate n a
source
theorem Multiset.le_replicate_iff {α : Type u_1} {m : Multiset α} {a : α} {n : ℕ} :
m ≤ replicate n a ↔ ∃ (k : ℕ), k ≤ n ∧ m = replicate k a
source
theorem Multiset.lt_replicate_succ {α : Type u_1} {m : Multiset α} {x : α} {n : ℕ} :
m < replicate (n + 1) x ↔ m ≤ replicate n x

### Multiplicity of an element #

source
@[simp]
theorem Multiset.count_replicate_self {α : Type u_1} [DecidableEq α] (a : α) (n : ℕ) :
count a (replicate n a) = n
source
theorem Multiset.count_replicate {α : Type u_1} [DecidableEq α] (a b : α) (n : ℕ) :
count a (replicate n b) = if b = a then n else 0
source
theorem Multiset.le_count_iff_replicate_le {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} {n : ℕ} :
n ≤ count a s ↔ replicate n a ≤ s

### Lift a relation to `Multiset`s #

source
theorem Multiset.rel_replicate_left {α : Type u_1} {m : Multiset α} {a : α} {r : α → α → Prop} {n : ℕ} :
Rel r (replicate n a) m ↔ m.card = n ∧ ∀ (x : α), x ∈ m → r a x
source
theorem Multiset.rel_replicate_right {α : Type u_1} {m : Multiset α} {a : α} {r : α → α → Prop} {n : ℕ} :
Rel r m (replicate n a) ↔ m.card = n ∧ ∀ (x : α), x ∈ m → r x a
source
theorem Multiset.nodup_iff_le {α : Type u_1} {s : Multiset α} :
s.Nodup ↔ ∀ (a : α), ¬a ::ₘ a ::ₘ 0 ≤ s
source
theorem Multiset.nodup_iff_ne_cons_cons {α : Type u_1} {s : Multiset α} :
s.Nodup ↔ ∀ (a : α) (t : Multiset α), s ≠ a ::ₘ a ::ₘ t
source
theorem Multiset.nodup_iff_pairwise {α : Type u_3} {s : Multiset α} :
s.Nodup ↔ Pairwise (fun (x1 x2 : α) => x1 ≠ x2) s
source
theorem Multiset.Nodup.pairwise {α : Type u_1} {r : α → α → Prop} {s : Multiset α} :
(∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ≠ b → r a b) → s.Nodup → Pairwise r s