Documentation

Mathlib.Data.Multiset.Replicate

Repeating elements in multisets #

Main definitions #

Multiset.replicate #

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

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

Equations
    Instances For
      theorem Multiset.coe_replicate {α : Type u_1} (n : ) (a : α) :
      @[simp]
      theorem Multiset.replicate_zero {α : Type u_1} (a : α) :
      replicate 0 a = 0
      @[simp]
      theorem Multiset.replicate_succ {α : Type u_1} (a : α) (n : ) :
      replicate (n + 1) a = a ::ₘ replicate n a
      theorem Multiset.replicate_add {α : Type u_1} (m n : ) (a : α) :
      replicate (m + n) a = replicate m a + replicate n a
      theorem Multiset.replicate_one {α : Type u_1} (a : α) :
      @[simp]
      theorem Multiset.card_replicate {α : Type u_1} (n : ) (a : α) :
      (replicate n a).card = n
      theorem Multiset.mem_replicate {α : Type u_1} {a b : α} {n : } :
      b replicate n a n 0 b = a
      theorem Multiset.eq_of_mem_replicate {α : Type u_1} {a b : α} {n : } :
      b replicate n ab = a
      theorem Multiset.eq_replicate_card {α : Type u_1} {a : α} {s : Multiset α} :
      s = replicate s.card a ∀ (b : α), b sb = a
      theorem Multiset.eq_replicate_of_mem {α : Type u_1} {a : α} {s : Multiset α} :
      (∀ (b : α), b sb = a)s = replicate s.card a

      Alias of the reverse direction of Multiset.eq_replicate_card.

      theorem Multiset.eq_replicate {α : Type u_1} {a : α} {n : } {s : Multiset α} :
      s = replicate n a s.card = n ∀ (b : α), b sb = a
      @[simp]
      theorem Multiset.replicate_right_inj {α : Type u_1} {a b : α} {n : } (h : n 0) :
      replicate n a = replicate n b a = b
      theorem Multiset.replicate_left_injective {α : Type u_1} (a : α) :
      theorem Multiset.replicate_subset_singleton {α : Type u_1} (n : ) (a : α) :
      theorem Multiset.replicate_le_coe {α : Type u_1} {a : α} {n : } {l : List α} :
      theorem Multiset.replicate_le_replicate {α : Type u_1} (a : α) {k n : } :
      theorem Multiset.replicate_mono {α : Type u_1} (a : α) {k n : } (h : k n) :
      theorem Multiset.le_replicate_iff {α : Type u_1} {m : Multiset α} {a : α} {n : } :
      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 #

      @[simp]
      theorem Multiset.count_replicate_self {α : Type u_1} [DecidableEq α] (a : α) (n : ) :
      count a (replicate n a) = n
      theorem Multiset.count_replicate {α : Type u_1} [DecidableEq α] (a b : α) (n : ) :
      count a (replicate n b) = if b = a then n else 0
      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 Multisets #

      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 mr a x
      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 mr x a
      theorem Multiset.nodup_iff_le {α : Type u_1} {s : Multiset α} :
      s.Nodup ∀ (a : α), ¬a ::ₘ a ::ₘ 0 s
      theorem Multiset.nodup_iff_ne_cons_cons {α : Type u_1} {s : Multiset α} :
      s.Nodup ∀ (a : α) (t : Multiset α), s a ::ₘ a ::ₘ t
      theorem Multiset.nodup_iff_pairwise {α : Type u_3} {s : Multiset α} :
      s.Nodup Pairwise (fun (x1 x2 : α) => x1 x2) s
      theorem Multiset.Nodup.pairwise {α : Type u_1} {r : ααProp} {s : Multiset α} :
      (∀ (a : α), a s∀ (b : α), b sa br a b)s.NodupPairwise r s