Loogle!

Result

Found 532 declarations mentioning Multiset.map. Of these, only the first 200 are shown.

• Multiset.map 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} (f : α → β) (s : Multiset α) : Multiset β
• Multiset.map_id 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} (s : Multiset α) : Multiset.map id s = s
• Multiset.map_id' 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} (s : Multiset α) : Multiset.map (fun x => x) s = s
• Multiset.Nodup.of_map 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} {s : Multiset α} (f : α → β) : (Multiset.map f s).Nodup → s.Nodup
• Multiset.map_injective 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} {f : α → β} (hf : Function.Injective f) : Function.Injective (Multiset.map f)
• Multiset.map_surjective_of_surjective 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} {f : α → β} (hf : Function.Surjective f) : Function.Surjective (Multiset.map f)
• Multiset.card_map 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} (f : α → β) (s : Multiset α) : (Multiset.map f s).card = s.card
• Multiset.map_const' 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} (s : Multiset α) (b : β) : Multiset.map (fun x => b) s = Multiset.replicate s.card b
• Multiset.Nodup.map 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} {f : α → β} {s : Multiset α} (hf : Function.Injective f) : s.Nodup → (Multiset.map f s).Nodup
• Multiset.nodup_map_iff_of_injective 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} {s : Multiset α} {f : α → β} (d : Function.Injective f) : (Multiset.map f s).Nodup ↔ s.Nodup
• Multiset.map_const 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} (s : Multiset α) (b : β) : Multiset.map (Function.const α b) s = Multiset.replicate s.card b
• Multiset.map_replicate 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} (f : α → β) (k : ℕ) (a : α) : Multiset.map f (Multiset.replicate k a) = Multiset.replicate k (f a)
• Multiset.map_coe 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} (f : α → β) (l : List α) : Multiset.map f ↑l = ↑(List.map f l)
• Multiset.map_mono 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} (f : α → β) : Monotone (Multiset.map f)
• Multiset.map_strictMono 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} (f : α → β) : StrictMono (Multiset.map f)
• Multiset.eq_of_mem_map_const 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} {b₁ b₂ : β} {l : List α} (h : b₁ ∈ Multiset.map (Function.const α b₂) ↑l) : b₁ = b₂
• Multiset.induction_on_multiset_quot 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {r : α → α → Prop} {p : Multiset (Quot r) → Prop} (s : Multiset (Quot r)) : (∀ (s : Multiset α), p (Multiset.map (Quot.mk r) s)) → p s
• Multiset.map_cons 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} (f : α → β) (a : α) (s : Multiset α) : Multiset.map f (a ::ₘ s) = f a ::ₘ Multiset.map f s
• Multiset.map_singleton 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} (f : α → β) (a : α) : Multiset.map f {a} = {f a}
• Multiset.exists_multiset_eq_map_quot_mk 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {r : α → α → Prop} (s : Multiset (Quot r)) : ∃ t, s = Multiset.map (Quot.mk r) t
• Multiset.mem_map_of_mem 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} (f : α → β) {a : α} {s : Multiset α} (h : a ∈ s) : f a ∈ Multiset.map f s
• Multiset.map_zero 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} (f : α → β) : Multiset.map f 0 = 0
• Multiset.map_subset_map 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} {f : α → β} {s t : Multiset α} (H : s ⊆ t) : Multiset.map f s ⊆ Multiset.map f t
• Multiset.map_eq_map 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} {f : α → β} (hf : Function.Injective f) {s t : Multiset α} : Multiset.map f s = Multiset.map f t ↔ s = t
• Multiset.map_map 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} {γ : Type u_2} (g : β → γ) (f : α → β) (s : Multiset α) : Multiset.map g (Multiset.map f s) = Multiset.map (g ∘ f) s
• Multiset.canLift 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} (c : β → α) (p : α → Prop) [CanLift α β c p] : CanLift (Multiset α) (Multiset β) (Multiset.map c) fun s => ∀ x ∈ s, p x
• Multiset.mem_map_of_injective 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} {f : α → β} (H : Function.Injective f) {a : α} {s : Multiset α} : f a ∈ Multiset.map f s ↔ a ∈ s
• Multiset.attach_map_val 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} (s : Multiset α) : Multiset.map Subtype.val s.attach = s
• Multiset.rel_map_left 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} {γ : Type u_2} {r : α → β → Prop} {s : Multiset γ} {f : γ → α} {t : Multiset β} : Multiset.Rel r (Multiset.map f s) t ↔ Multiset.Rel (fun a b => r (f a) b) s t
• Multiset.rel_map_right 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} {γ : Type u_2} {r : α → β → Prop} {s : Multiset α} {t : Multiset γ} {f : γ → β} : Multiset.Rel r s (Multiset.map f t) ↔ Multiset.Rel (fun a b => r a (f b)) s t
• Multiset.forall_mem_map_iff 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} {f : α → β} {p : β → Prop} {s : Multiset α} : (∀ y ∈ Multiset.map f s, p y) ↔ ∀ x ∈ s, p (f x)
• Multiset.map_eq_zero 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} {s : Multiset α} {f : α → β} : Multiset.map f s = 0 ↔ s = 0
• Multiset.map_erase 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} [DecidableEq α] [DecidableEq β] (f : α → β) (hf : Function.Injective f) (x : α) (s : Multiset α) : Multiset.map f (s.erase x) = (Multiset.map f s).erase (f x)
• Multiset.map_mk_eq_map_mk_of_rel 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {r : α → α → Prop} {s t : Multiset α} (hst : Multiset.Rel r s t) : Multiset.map (Quot.mk r) s = Multiset.map (Quot.mk r) t
• Multiset.mem_map 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} {f : α → β} {b : β} {s : Multiset α} : b ∈ Multiset.map f s ↔ ∃ a ∈ s, f a = b
• Multiset.pmap_eq_map 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} (p : α → Prop) (f : α → β) (s : Multiset α) (H : ∀ a ∈ s, p a) : Multiset.pmap (fun a x => f a) s H = Multiset.map f s
• Multiset.map_comp_cons 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} (f : α → β) (t : α) : Multiset.map f ∘ Multiset.cons t = Multiset.cons (f t) ∘ Multiset.map f
• Multiset.inj_on_of_nodup_map 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} {f : α → β} {s : Multiset α} : (Multiset.map f s).Nodup → ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y
• Multiset.map_erase_of_mem 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} [DecidableEq α] [DecidableEq β] (f : α → β) (s : Multiset α) {x : α} (h : x ∈ s) : Multiset.map f (s.erase x) = (Multiset.map f s).erase (f x)
• Multiset.map_le_map 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} {f : α → β} {s t : Multiset α} (h : s ≤ t) : Multiset.map f s ≤ Multiset.map f t
• Multiset.map_lt_map 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} {f : α → β} {s t : Multiset α} (h : s < t) : Multiset.map f s < Multiset.map f t
• Multiset.rel_map 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} {γ : Type u_2} {δ : Type u_3} {p : γ → δ → Prop} {s : Multiset α} {t : Multiset β} {f : α → γ} {g : β → δ} : Multiset.Rel p (Multiset.map f s) (Multiset.map g t) ↔ Multiset.Rel (fun a b => p (f a) (g b)) s t
• Multiset.map_congr 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} {f g : α → β} {s t : Multiset α} : s = t → (∀ x ∈ t, f x = g x) → Multiset.map f s = Multiset.map g t
• Multiset.map_eq_singleton 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} {f : α → β} {s : Multiset α} {b : β} : Multiset.map f s = {b} ↔ ∃ a, s = {a} ∧ f a = b
• Multiset.map_hcongr 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β β' : Type v} {m : Multiset α} {f : α → β} {f' : α → β'} (h : β = β') (hf : ∀ a ∈ m, HEq (f a) (f' a)) : HEq (Multiset.map f m) (Multiset.map f' m)
• Multiset.Nodup.map_on 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} {s : Multiset α} {f : α → β} : (∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y) → s.Nodup → (Multiset.map f s).Nodup
• Multiset.nodup_map_iff_inj_on 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} {f : α → β} {s : Multiset α} (d : s.Nodup) : (Multiset.map f s).Nodup ↔ ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y
• Multiset.nodup_map_iff_of_inj_on 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} {s : Multiset α} {f : α → β} (d : ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y) : (Multiset.map f s).Nodup ↔ s.Nodup
• Multiset.map_add 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} (f : α → β) (s t : Multiset α) : Multiset.map f (s + t) = Multiset.map f s + Multiset.map f t
• Multiset.map_pmap 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} {γ : Type u_2} {p : α → Prop} (g : β → γ) (f : (a : α) → p a → β) (s : Multiset α) (H : ∀ a ∈ s, p a) : Multiset.map g (Multiset.pmap f s H) = Multiset.pmap (fun a h => g (f a h)) s H
• Multiset.attach_map_val' 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} (s : Multiset α) (f : α → β) : Multiset.map (fun i => f ↑i) s.attach = Multiset.map f s
• Multiset.map_eq_cons 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} [DecidableEq α] (f : α → β) (s : Multiset α) (t : Multiset β) (b : β) : (∃ a ∈ s, f a = b ∧ Multiset.map f (s.erase a) = t) ↔ Multiset.map f s = b ::ₘ t
• Multiset.pmap_eq_map_attach 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} {p : α → Prop} (f : (a : α) → p a → β) (s : Multiset α) (H : ∀ a ∈ s, p a) : Multiset.pmap f s H = Multiset.map (fun x => f ↑x ⋯) s.attach
• Multiset.erase_attach_map_val 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} [DecidableEq α] (s : Multiset α) (x : { x // x ∈ s }) : Multiset.map Subtype.val (s.attach.erase x) = s.erase ↑x
• Multiset.erase_attach_map 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} [DecidableEq α] (s : Multiset α) (f : α → β) (x : { x // x ∈ s }) : Multiset.map (fun j => f ↑j) (s.attach.erase x) = Multiset.map f (s.erase ↑x)
• Multiset.map_eq_map_of_bij_of_nodup 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} {β : Type v} {γ : Type u_2} (f : α → γ) (g : β → γ) {s : Multiset α} {t : Multiset β} (hs : s.Nodup) (ht : t.Nodup) (i : (a : α) → a ∈ s → β) (hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t) (i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂) (i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b) (h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)) : Multiset.map f s = Multiset.map g t
• Multiset.attach_cons 📋 Mathlib.Data.Multiset.MapFold
  {α : Type u_1} (a : α) (m : Multiset α) : (a ::ₘ m).attach = ⟨a, ⋯⟩ ::ₘ Multiset.map (fun p => ⟨↑p, ⋯⟩) m.attach
• Multiset.filterMap_eq_map 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} {β : Type v} (f : α → β) : Multiset.filterMap (some ∘ f) = Multiset.map f
• Multiset.count_map_eq_count' 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} {β : Type v} [DecidableEq α] [DecidableEq β] (f : α → β) (s : Multiset α) (hf : Function.Injective f) (x : α) : Multiset.count (f x) (Multiset.map f s) = Multiset.count x s
• Multiset.map_count_True_eq_filter_card 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} (s : Multiset α) (p : α → Prop) [DecidablePred p] : Multiset.count True (Multiset.map p s) = (Multiset.filter p s).card
• Multiset.filterMap_map 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} {β : Type v} {γ : Type u_2} (f : α → β) (g : β → Option γ) (s : Multiset α) : Multiset.filterMap g (Multiset.map f s) = Multiset.filterMap (g ∘ f) s
• Multiset.map_filterMap 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} {β : Type v} {γ : Type u_2} (f : α → Option β) (g : β → γ) (s : Multiset α) : Multiset.map g (Multiset.filterMap f s) = Multiset.filterMap (fun x => Option.map g (f x)) s
• Multiset.countP_map 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} {β : Type v} (f : α → β) (s : Multiset α) (p : β → Prop) [DecidablePred p] : Multiset.countP p (Multiset.map f s) = (Multiset.filter (fun a => p (f a)) s).card
• Multiset.map_filterMap_of_inv 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} {β : Type v} (f : α → Option β) (g : β → α) (H : ∀ (x : α), Option.map g (f x) = some x) (s : Multiset α) : Multiset.map g (Multiset.filterMap f s) = s
• Multiset.count_map 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_3} {β : Type u_4} (f : α → β) (s : Multiset α) [DecidableEq β] (b : β) : Multiset.count b (Multiset.map f s) = (Multiset.filter (fun a => b = f a) s).card
• Multiset.filter_map 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} {β : Type v} (p : α → Prop) [DecidablePred p] (f : β → α) (s : Multiset β) : Multiset.filter p (Multiset.map f s) = Multiset.map f (Multiset.filter (p ∘ f) s)
• Multiset.map_le_map_iff 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} {β : Type v} {f : α → β} (hf : Function.Injective f) {s t : Multiset α} : Multiset.map f s ≤ Multiset.map f t ↔ s ≤ t
• Multiset.count_map_eq_count 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} {β : Type v} [DecidableEq α] [DecidableEq β] (f : α → β) (s : Multiset α) (hf : Set.InjOn f {x | x ∈ s}) (x : α) (H : x ∈ s) : Multiset.count (f x) (Multiset.map f s) = Multiset.count x s
• Multiset.map_filter' 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} {β : Type v} (p : α → Prop) [DecidablePred p] {f : α → β} (hf : Function.Injective f) (s : Multiset α) [DecidablePred fun b => ∃ a, p a ∧ f a = b] : Multiset.map f (Multiset.filter p s) = Multiset.filter (fun b => ∃ a, p a ∧ f a = b) (Multiset.map f s)
• Multiset.mapEmbedding_apply 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} {β : Type v} (f : α ↪ β) (s : Multiset α) : (Multiset.mapEmbedding f) s = Multiset.map (⇑f) s
• Multiset.filter_attach 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} (s : Multiset α) (p : α → Prop) [DecidablePred p] : Multiset.filter (fun a => p ↑a) s.attach = Multiset.map (Subtype.map id ⋯) (Multiset.filter p s).attach
• Multiset.filter_attach' 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} (s : Multiset α) (p : { a // a ∈ s } → Prop) [DecidableEq α] [DecidablePred p] : Multiset.filter p s.attach = Multiset.map (Subtype.map id ⋯) (Multiset.filter (fun x => ∃ (h : x ∈ s), p ⟨x, h⟩) s).attach
• Multiset.prod_map_one 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Defs
  {ι : Type u_2} {α : Type u_3} [CommMonoid α] {m : Multiset ι} : (Multiset.map (fun x => 1) m).prod = 1
• Multiset.sum_map_zero 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Defs
  {ι : Type u_2} {α : Type u_3} [AddCommMonoid α] {m : Multiset ι} : (Multiset.map (fun x => 0) m).sum = 0
• Multiset.prod_hom_rel 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Defs
  {ι : Type u_2} {α : Type u_3} {β : Type u_4} [CommMonoid α] [CommMonoid β] (s : Multiset ι) {r : α → β → Prop} {f : ι → α} {g : ι → β} (h₁ : r 1 1) (h₂ : ∀ ⦃a : ι⦄ ⦃b : α⦄ ⦃c : β⦄, r b c → r (f a * b) (g a * c)) : r (Multiset.map f s).prod (Multiset.map g s).prod
• Multiset.sum_hom_rel 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Defs
  {ι : Type u_2} {α : Type u_3} {β : Type u_4} [AddCommMonoid α] [AddCommMonoid β] (s : Multiset ι) {r : α → β → Prop} {f : ι → α} {g : ι → β} (h₁ : r 0 0) (h₂ : ∀ ⦃a : ι⦄ ⦃b : α⦄ ⦃c : β⦄, r b c → r (f a + b) (g a + c)) : r (Multiset.map f s).sum (Multiset.map g s).sum
• Multiset.map_set_pairwise 📋 Mathlib.Data.Multiset.UnionInter
  {α : Type u_1} {β : Type v} {f : α → β} {r : β → β → Prop} {m : Multiset α} (h : {a | a ∈ m}.Pairwise fun a₁ a₂ => r (f a₁) (f a₂)) : {b | b ∈ Multiset.map f m}.Pairwise r
• Multiset.map_union 📋 Mathlib.Data.Multiset.UnionInter
  {α : Type u_1} {β : Type v} [DecidableEq α] [DecidableEq β] {f : α → β} (finj : Function.Injective f) {s t : Multiset α} : Multiset.map f (s ∪ t) = Multiset.map f s ∪ Multiset.map f t
• Multiset.disjoint_map_map 📋 Mathlib.Data.Multiset.UnionInter
  {α : Type u_1} {β : Type v} {γ : Type u_2} {f : α → γ} {g : β → γ} {s : Multiset α} {t : Multiset β} : Disjoint (Multiset.map f s) (Multiset.map g t) ↔ ∀ a ∈ s, ∀ b ∈ t, f a ≠ g b
• Multiset.dedup_map_dedup_eq 📋 Mathlib.Data.Multiset.Dedup
  {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (f : α → β) (s : Multiset α) : (Multiset.map f s.dedup).dedup = (Multiset.map f s).dedup
• Multiset.dedup_map_of_injective 📋 Mathlib.Data.Multiset.Dedup
  {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {f : α → β} (hf : Function.Injective f) (s : Multiset α) : (Multiset.map f s).dedup = Multiset.map f s.dedup
• Multiset.attach_ndinsert 📋 Mathlib.Data.Multiset.FinsetOps
  {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) : (Multiset.ndinsert a s).attach = Multiset.ndinsert ⟨a, ⋯⟩ (Multiset.map (fun p => ⟨↑p, ⋯⟩) s.attach)
• Multiset.range_disjoint_map_add 📋 Mathlib.Data.Multiset.Range
  (a : ℕ) (m : Multiset ℕ) : Disjoint (Multiset.range a) (Multiset.map (fun x => a + x) m)
• Multiset.range_add_eq_union 📋 Mathlib.Data.Multiset.Range
  (a b : ℕ) : Multiset.range (a + b) = Multiset.range a ∪ Multiset.map (fun x => a + x) (Multiset.range b)
• Multiset.range_add 📋 Mathlib.Data.Multiset.Range
  (a b : ℕ) : Multiset.range (a + b) = Multiset.range a + Multiset.map (fun x => a + x) (Multiset.range b)
• Finset.image_val 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : α → β) (s : Finset α) : (Finset.image f s).val = (Multiset.map f s.val).dedup
• Finset.image_toFinset 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} [DecidableEq α] {s : Multiset α} : Finset.image f s.toFinset = (Multiset.map f s).toFinset
• Multiset.toFinset_map 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (f : α → β) (m : Multiset α) : (Multiset.map f m).toFinset = Finset.image f m.toFinset
• Finset.image_val_of_injOn 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → β} {s : Finset α} (H : Set.InjOn f ↑s) : (Finset.image f s).val = Multiset.map f s.val
• Finset.map_val 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Finset α) : (Finset.map f s).val = Multiset.map (⇑f) s.val
• Finset.map_toFinset 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} {β : Type u_2} {f : α ↪ β} [DecidableEq α] [DecidableEq β] {s : Multiset α} : Finset.map f s.toFinset = (Multiset.map (⇑f) s).toFinset
• Fintype.nodup_map_univ_iff_injective 📋 Mathlib.Data.Fintype.Defs
  {α : Type u_1} {β : Type u_2} [Fintype α] {f : α → β} : (Multiset.map f Finset.univ.val).Nodup ↔ Function.Injective f
• Finset.nodup_map_iff_injOn 📋 Mathlib.Data.Fintype.Defs
  {α : Type u_1} {β : Type u_2} {f : α → β} {s : Finset α} : (Multiset.map f s.val).Nodup ↔ Set.InjOn f ↑s
• Finset.univ_val_map_subtype_val 📋 Mathlib.Data.Finset.BooleanAlgebra
  {α : Type u_1} [Fintype α] (p : α → Prop) [DecidablePred p] [Fintype { a // p a }] : Multiset.map Subtype.val Finset.univ.val = (Finset.filter p Finset.univ).val
• Finset.univ_val_map_subtype_restrict 📋 Mathlib.Data.Finset.BooleanAlgebra
  {α : Type u_1} {β : Type u_2} [Fintype α] (f : α → β) (p : α → Prop) [DecidablePred p] [Fintype { a // p a }] : Multiset.map (Subtype.restrict p f) Finset.univ.val = Multiset.map f (Finset.filter p Finset.univ).val
• Multiset.fold_hom 📋 Mathlib.Data.Multiset.Fold
  {α : Type u_1} {β : Type u_2} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] {op' : β → β → β} [Std.Commutative op'] [Std.Associative op'] {m : α → β} (hm : ∀ (x y : α), m (op x y) = op' (m x) (m y)) (b : α) (s : Multiset α) : Multiset.fold op' (m b) (Multiset.map m s) = m (Multiset.fold op b s)
• Multiset.fold_distrib 📋 Mathlib.Data.Multiset.Fold
  {α : Type u_1} {β : Type u_2} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] {f g : β → α} (u₁ u₂ : α) (s : Multiset β) : Multiset.fold op (op u₁ u₂) (Multiset.map (fun x => op (f x) (g x)) s) = op (Multiset.fold op u₁ (Multiset.map f s)) (Multiset.fold op u₂ (Multiset.map g s))
• Multiset.map_nsmul 📋 Mathlib.Algebra.Order.Group.Multiset
  {α : Type u_1} {β : Type u_2} (f : α → β) (n : ℕ) (s : Multiset α) : Multiset.map f (n • s) = n • Multiset.map f s
• Multiset.coe_mapAddMonoidHom 📋 Mathlib.Algebra.Order.Group.Multiset
  {α : Type u_1} {β : Type u_2} (f : α → β) : ⇑(Multiset.mapAddMonoidHom f) = Multiset.map f
• Multiset.mapAddMonoidHom_apply 📋 Mathlib.Algebra.Order.Group.Multiset
  {α : Type u_1} {β : Type u_2} (f : α → β) (s : Multiset α) : (Multiset.mapAddMonoidHom f) s = Multiset.map f s
• Multiset.sum_map_singleton 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {α : Type u_3} (s : Multiset α) : (Multiset.map (fun a => {a}) s).sum = s
• Multiset.fst_prod 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {α : Type u_3} {β : Type u_4} [CommMonoid α] [CommMonoid β] (s : Multiset (α × β)) : s.prod.1 = (Multiset.map Prod.fst s).prod
• Multiset.fst_sum 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {α : Type u_3} {β : Type u_4} [AddCommMonoid α] [AddCommMonoid β] (s : Multiset (α × β)) : s.sum.1 = (Multiset.map Prod.fst s).sum
• Multiset.snd_prod 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {α : Type u_3} {β : Type u_4} [CommMonoid α] [CommMonoid β] (s : Multiset (α × β)) : s.prod.2 = (Multiset.map Prod.snd s).prod
• Multiset.snd_sum 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {α : Type u_3} {β : Type u_4} [AddCommMonoid α] [AddCommMonoid β] (s : Multiset (α × β)) : s.sum.2 = (Multiset.map Prod.snd s).sum
• Multiset.prod_int_mod 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  (s : Multiset ℤ) (n : ℤ) : s.prod % n = (Multiset.map (fun x => x % n) s).prod % n
• Multiset.prod_nat_mod 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  (s : Multiset ℕ) (n : ℕ) : s.prod % n = (Multiset.map (fun x => x % n) s).prod % n
• Multiset.sum_int_mod 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  (s : Multiset ℤ) (n : ℤ) : s.sum % n = (Multiset.map (fun x => x % n) s).sum % n
• Multiset.sum_nat_mod 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  (s : Multiset ℕ) (n : ℕ) : s.sum % n = (Multiset.map (fun x => x % n) s).sum % n
• Multiset.prod_map_inv' 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {α : Type u_3} [DivisionCommMonoid α] (m : Multiset α) : (Multiset.map Inv.inv m).prod = m.prod⁻¹
• Multiset.sum_map_neg' 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {α : Type u_3} [SubtractionCommMonoid α] (m : Multiset α) : (Multiset.map Neg.neg m).sum = -m.sum
• Multiset.prod_map_prod_map 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {α : Type u_3} {β' : Type u_5} {γ : Type u_6} [CommMonoid α] (m : Multiset β') (n : Multiset γ) {f : β' → γ → α} : (Multiset.map (fun a => (Multiset.map (fun b => f a b) n).prod) m).prod = (Multiset.map (fun b => (Multiset.map (fun a => f a b) m).prod) n).prod
• Multiset.sum_map_sum_map 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {α : Type u_3} {β' : Type u_5} {γ : Type u_6} [AddCommMonoid α] (m : Multiset β') (n : Multiset γ) {f : β' → γ → α} : (Multiset.map (fun a => (Multiset.map (fun b => f a b) n).sum) m).sum = (Multiset.map (fun b => (Multiset.map (fun a => f a b) m).sum) n).sum
• Multiset.prod_map_inv 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {ι : Type u_2} {α : Type u_3} [DivisionCommMonoid α] {m : Multiset ι} {f : ι → α} : (Multiset.map (fun i => (f i)⁻¹) m).prod = (Multiset.map f m).prod⁻¹
• Multiset.sum_map_neg 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {ι : Type u_2} {α : Type u_3} [SubtractionCommMonoid α] {m : Multiset ι} {f : ι → α} : (Multiset.map (fun i => -f i) m).sum = -(Multiset.map f m).sum
• Multiset.prod_map_pow 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {ι : Type u_2} {α : Type u_3} [CommMonoid α] {m : Multiset ι} {f : ι → α} {n : ℕ} : (Multiset.map (fun i => f i ^ n) m).prod = (Multiset.map f m).prod ^ n
• Multiset.sum_map_nsmul 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {ι : Type u_2} {α : Type u_3} [AddCommMonoid α] {m : Multiset ι} {f : ι → α} {n : ℕ} : (Multiset.map (fun i => n • f i) m).sum = n • (Multiset.map f m).sum
• map_multiset_prod 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {F : Type u_1} {α : Type u_3} {β : Type u_4} [CommMonoid α] [CommMonoid β] [FunLike F α β] [MonoidHomClass F α β] (f : F) (s : Multiset α) : f s.prod = (Multiset.map (⇑f) s).prod
• map_multiset_sum 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {F : Type u_1} {α : Type u_3} {β : Type u_4} [AddCommMonoid α] [AddCommMonoid β] [FunLike F α β] [AddMonoidHomClass F α β] (f : F) (s : Multiset α) : f s.sum = (Multiset.map (⇑f) s).sum
• Multiset.prod_hom 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {α : Type u_3} {β : Type u_4} [CommMonoid α] [CommMonoid β] (s : Multiset α) {F : Type u_7} [FunLike F α β] [MonoidHomClass F α β] (f : F) : (Multiset.map (⇑f) s).prod = f s.prod
• Multiset.prod_map_erase 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {ι : Type u_2} {α : Type u_3} [CommMonoid α] {m : Multiset ι} {f : ι → α} [DecidableEq ι] {a : ι} (h : a ∈ m) : f a * (Multiset.map f (m.erase a)).prod = (Multiset.map f m).prod
• Multiset.sum_hom 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {α : Type u_3} {β : Type u_4} [AddCommMonoid α] [AddCommMonoid β] (s : Multiset α) {F : Type u_7} [FunLike F α β] [AddMonoidHomClass F α β] (f : F) : (Multiset.map (⇑f) s).sum = f s.sum
• Multiset.sum_map_erase 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {ι : Type u_2} {α : Type u_3} [AddCommMonoid α] {m : Multiset ι} {f : ι → α} [DecidableEq ι] {a : ι} (h : a ∈ m) : f a + (Multiset.map f (m.erase a)).sum = (Multiset.map f m).sum
• Multiset.prod_dvd_prod_of_dvd 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {α : Type u_3} {β : Type u_4} [CommMonoid β] {S : Multiset α} (g1 g2 : α → β) (h : ∀ a ∈ S, g1 a ∣ g2 a) : (Multiset.map g1 S).prod ∣ (Multiset.map g2 S).prod
• Multiset.prod_map_zpow 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {ι : Type u_2} {α : Type u_3} [DivisionCommMonoid α] {m : Multiset ι} {f : ι → α} {n : ℤ} : (Multiset.map (fun i => f i ^ n) m).prod = (Multiset.map f m).prod ^ n
• Multiset.sum_map_zsmul 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {ι : Type u_2} {α : Type u_3} [SubtractionCommMonoid α] {m : Multiset ι} {f : ι → α} {n : ℤ} : (Multiset.map (fun i => n • f i) m).sum = n • (Multiset.map f m).sum
• Multiset.prod_hom' 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {ι : Type u_2} {α : Type u_3} {β : Type u_4} [CommMonoid α] [CommMonoid β] (s : Multiset ι) {F : Type u_7} [FunLike F α β] [MonoidHomClass F α β] (f : F) (g : ι → α) : (Multiset.map (fun i => f (g i)) s).prod = f (Multiset.map g s).prod
• Multiset.prod_map_mul 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {ι : Type u_2} {α : Type u_3} [CommMonoid α] {m : Multiset ι} {f g : ι → α} : (Multiset.map (fun i => f i * g i) m).prod = (Multiset.map f m).prod * (Multiset.map g m).prod
• Multiset.sum_hom' 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {ι : Type u_2} {α : Type u_3} {β : Type u_4} [AddCommMonoid α] [AddCommMonoid β] (s : Multiset ι) {F : Type u_7} [FunLike F α β] [AddMonoidHomClass F α β] (f : F) (g : ι → α) : (Multiset.map (fun i => f (g i)) s).sum = f (Multiset.map g s).sum
• Multiset.sum_map_add 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {ι : Type u_2} {α : Type u_3} [AddCommMonoid α] {m : Multiset ι} {f g : ι → α} : (Multiset.map (fun i => f i + g i) m).sum = (Multiset.map f m).sum + (Multiset.map g m).sum
• Multiset.prod_map_eq_pow_single 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {ι : Type u_2} {α : Type u_3} [CommMonoid α] {m : Multiset ι} {f : ι → α} [DecidableEq ι] (i : ι) (hf : ∀ (i' : ι), i' ≠ i → i' ∈ m → f i' = 1) : (Multiset.map f m).prod = f i ^ Multiset.count i m
• Multiset.sum_map_eq_nsmul_single 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {ι : Type u_2} {α : Type u_3} [AddCommMonoid α] {m : Multiset ι} {f : ι → α} [DecidableEq ι] (i : ι) (hf : ∀ (i' : ι), i' ≠ i → i' ∈ m → f i' = 0) : (Multiset.map f m).sum = Multiset.count i m • f i
• Multiset.prod_map_div 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {ι : Type u_2} {α : Type u_3} [DivisionCommMonoid α] {m : Multiset ι} {f g : ι → α} : (Multiset.map (fun i => f i / g i) m).prod = (Multiset.map f m).prod / (Multiset.map g m).prod
• Multiset.sum_map_sub 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {ι : Type u_2} {α : Type u_3} [SubtractionCommMonoid α] {m : Multiset ι} {f g : ι → α} : (Multiset.map (fun i => f i - g i) m).sum = (Multiset.map f m).sum - (Multiset.map g m).sum
• map_multiset_ne_zero_prod 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {F : Type u_1} {α : Type u_3} {β : Type u_4} [CommMonoid α] [CommMonoid β] [FunLike F α β] [MulHomClass F α β] (f : F) {s : Multiset α} (hs : s ≠ 0) : f s.prod = (Multiset.map (⇑f) s).prod
• map_multiset_ne_zero_sum 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {F : Type u_1} {α : Type u_3} {β : Type u_4} [AddCommMonoid α] [AddCommMonoid β] [FunLike F α β] [AddHomClass F α β] (f : F) {s : Multiset α} (hs : s ≠ 0) : f s.sum = (Multiset.map (⇑f) s).sum
• Multiset.prod_hom_ne_zero 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {α : Type u_3} {β : Type u_4} [CommMonoid α] [CommMonoid β] {s : Multiset α} (hs : s ≠ 0) {F : Type u_7} [FunLike F α β] [MulHomClass F α β] (f : F) : (Multiset.map (⇑f) s).prod = f s.prod
• Multiset.sum_hom_ne_zero 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {α : Type u_3} {β : Type u_4} [AddCommMonoid α] [AddCommMonoid β] {s : Multiset α} (hs : s ≠ 0) {F : Type u_7} [FunLike F α β] [AddHomClass F α β] (f : F) : (Multiset.map (⇑f) s).sum = f s.sum
• AddMonoidHom.map_multiset_sum 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {α : Type u_3} {β : Type u_4} [AddCommMonoid α] [AddCommMonoid β] (f : α →+ β) (s : Multiset α) : f s.sum = (Multiset.map (⇑f) s).sum
• MonoidHom.map_multiset_prod 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {α : Type u_3} {β : Type u_4} [CommMonoid α] [CommMonoid β] (f : α →* β) (s : Multiset α) : f s.prod = (Multiset.map (⇑f) s).prod
• Multiset.prod_hom₂_ne_zero 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {ι : Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_6} [CommMonoid α] [CommMonoid β] [CommMonoid γ] {s : Multiset ι} (hs : s ≠ 0) (f : α → β → γ) (hf : ∀ (a b : α) (c d : β), f (a * b) (c * d) = f a c * f b d) (f₁ : ι → α) (f₂ : ι → β) : (Multiset.map (fun i => f (f₁ i) (f₂ i)) s).prod = f (Multiset.map f₁ s).prod (Multiset.map f₂ s).prod
• Multiset.sum_hom₂_ne_zero 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {ι : Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_6} [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] {s : Multiset ι} (hs : s ≠ 0) (f : α → β → γ) (hf : ∀ (a b : α) (c d : β), f (a + b) (c + d) = f a c + f b d) (f₁ : ι → α) (f₂ : ι → β) : (Multiset.map (fun i => f (f₁ i) (f₂ i)) s).sum = f (Multiset.map f₁ s).sum (Multiset.map f₂ s).sum
• AddHom.map_multiset_ne_zero_sum 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {α : Type u_3} {β : Type u_4} [AddCommMonoid α] [AddCommMonoid β] (f : α →ₙ+ β) (s : Multiset α) (hs : s ≠ 0) : f s.sum = (Multiset.map (⇑f) s).sum
• MulHom.map_multiset_ne_zero_prod 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {α : Type u_3} {β : Type u_4} [CommMonoid α] [CommMonoid β] (f : α →ₙ* β) (s : Multiset α) (hs : s ≠ 0) : f s.prod = (Multiset.map (⇑f) s).prod
• Multiset.prod_hom₂ 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {ι : Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_6} [CommMonoid α] [CommMonoid β] [CommMonoid γ] (s : Multiset ι) (f : α → β → γ) (hf : ∀ (a b : α) (c d : β), f (a * b) (c * d) = f a c * f b d) (hf' : f 1 1 = 1) (f₁ : ι → α) (f₂ : ι → β) : (Multiset.map (fun i => f (f₁ i) (f₂ i)) s).prod = f (Multiset.map f₁ s).prod (Multiset.map f₂ s).prod
• Multiset.sum_hom₂ 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {ι : Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_6} [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] (s : Multiset ι) (f : α → β → γ) (hf : ∀ (a b : α) (c d : β), f (a + b) (c + d) = f a c + f b d) (hf' : f 0 0 = 0) (f₁ : ι → α) (f₂ : ι → β) : (Multiset.map (fun i => f (f₁ i) (f₂ i)) s).sum = f (Multiset.map f₁ s).sum (Multiset.map f₂ s).sum
• Multiset.sum_map_tsub 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {ι : Type u_2} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2] [ContravariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2] [Sub α] [OrderedSub α] (l : Multiset ι) {f g : ι → α} (hfg : ∀ x ∈ l, g x ≤ f x) : (Multiset.map (fun x => f x - g x) l).sum = (Multiset.map f l).sum - (Multiset.map g l).sum
• Multiset.card_join 📋 Mathlib.Data.Multiset.Bind
  {α : Type u_1} (S : Multiset (Multiset α)) : S.join.card = (Multiset.map Multiset.card S).sum
• Multiset.bind.eq_1 📋 Mathlib.Data.Multiset.Bind
  {α : Type u_1} {β : Type v} (s : Multiset α) (f : α → Multiset β) : s.bind f = (Multiset.map f s).join
• Multiset.prod_join 📋 Mathlib.Data.Multiset.Bind
  {α : Type u_1} [CommMonoid α] {S : Multiset (Multiset α)} : S.join.prod = (Multiset.map Multiset.prod S).prod
• Multiset.sum_join 📋 Mathlib.Data.Multiset.Bind
  {α : Type u_1} [AddCommMonoid α] {S : Multiset (Multiset α)} : S.join.sum = (Multiset.map Multiset.sum S).sum
• Multiset.bind_singleton 📋 Mathlib.Data.Multiset.Bind
  {α : Type u_1} {β : Type v} (s : Multiset α) (f : α → β) : (s.bind fun x => {f x}) = Multiset.map f s
• Multiset.map_join 📋 Mathlib.Data.Multiset.Bind
  {α : Type u_1} {β : Type v} (f : α → β) (S : Multiset (Multiset α)) : Multiset.map f S.join = (Multiset.map (Multiset.map f) S).join
• Multiset.bind_map 📋 Mathlib.Data.Multiset.Bind
  {α : Type u_1} {β : Type v} {γ : Type u_2} (m : Multiset α) (n : β → Multiset γ) (f : α → β) : (Multiset.map f m).bind n = m.bind fun a => n (f a)
• Multiset.card_bind 📋 Mathlib.Data.Multiset.Bind
  {α : Type u_1} {β : Type v} (s : Multiset α) (f : α → Multiset β) : (s.bind f).card = (Multiset.map (Multiset.card ∘ f) s).sum
• Multiset.prod_bind 📋 Mathlib.Data.Multiset.Bind
  {α : Type u_1} {β : Type v} [CommMonoid β] (s : Multiset α) (t : α → Multiset β) : (s.bind t).prod = (Multiset.map (fun a => (t a).prod) s).prod
• Multiset.sum_bind 📋 Mathlib.Data.Multiset.Bind
  {α : Type u_1} {β : Type v} [AddCommMonoid β] (s : Multiset α) (t : α → Multiset β) : (s.bind t).sum = (Multiset.map (fun a => (t a).sum) s).sum
• Multiset.map_bind 📋 Mathlib.Data.Multiset.Bind
  {α : Type u_1} {β : Type v} {γ : Type u_2} (m : Multiset α) (n : α → Multiset β) (f : β → γ) : Multiset.map f (m.bind n) = m.bind fun a => Multiset.map f (n a)
• Multiset.product.eq_1 📋 Mathlib.Data.Multiset.Bind
  {α : Type u_1} {β : Type v} (s : Multiset α) (t : Multiset β) : s.product t = s.bind fun a => Multiset.map (Prod.mk a) t
• Multiset.card_sigma 📋 Mathlib.Data.Multiset.Bind
  {α : Type u_1} {σ : α → Type u_4} (s : Multiset α) (t : (a : α) → Multiset (σ a)) : (s.sigma t).card = (Multiset.map (fun a => (t a).card) s).sum
• Multiset.count_bind 📋 Mathlib.Data.Multiset.Bind
  {α : Type u_1} {β : Type v} [DecidableEq α] {m : Multiset β} {f : β → Multiset α} {a : α} : Multiset.count a (m.bind f) = (Multiset.map (fun b => Multiset.count a (f b)) m).sum
• Multiset.bind_map_comm 📋 Mathlib.Data.Multiset.Bind
  {α : Type u_1} {β : Type v} {γ : Type u_2} (m : Multiset α) (n : Multiset β) {f : α → β → γ} : (m.bind fun a => Multiset.map (fun b => f a b) n) = n.bind fun b => Multiset.map (fun a => f a b) m
• Multiset.count_sum 📋 Mathlib.Data.Multiset.Bind
  {α : Type u_1} {β : Type v} [DecidableEq α] {m : Multiset β} {f : β → Multiset α} {a : α} : Multiset.count a (Multiset.map f m).sum = (Multiset.map (fun b => Multiset.count a (f b)) m).sum
• Multiset.bind_cons 📋 Mathlib.Data.Multiset.Bind
  {α : Type u_1} {β : Type v} (s : Multiset α) (f : α → β) (g : α → Multiset β) : (s.bind fun a => f a ::ₘ g a) = Multiset.map f s + s.bind g
• Multiset.sigma.eq_1 📋 Mathlib.Data.Multiset.Bind
  {α : Type u_1} {σ : α → Type u_4} (s : Multiset α) (t : (a : α) → Multiset (σ a)) : s.sigma t = s.bind fun a => Multiset.map (Sigma.mk a) (t a)
• Multiset.fold_bind 📋 Mathlib.Data.Multiset.Bind
  {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] {ι : Type u_4} (s : Multiset ι) (t : ι → Multiset α) (b : ι → α) (b₀ : α) : Multiset.fold op (Multiset.fold op b₀ (Multiset.map b s)) (s.bind t) = Multiset.fold op b₀ (Multiset.map (fun i => Multiset.fold op (b i) (t i)) s)
• Multiset.cons_sigma 📋 Mathlib.Data.Multiset.Bind
  {α : Type u_1} {σ : α → Type u_4} (a : α) (s : Multiset α) (t : (a : α) → Multiset (σ a)) : (a ::ₘ s).sigma t = Multiset.map (Sigma.mk a) (t a) + s.sigma t
• Multiset.cons_product 📋 Mathlib.Data.Multiset.Bind
  {α : Type u_1} {β : Type v} (a : α) (s : Multiset α) (t : Multiset β) : (a ::ₘ s) ×ˢ t = Multiset.map (Prod.mk a) t + s ×ˢ t
• Multiset.product_cons 📋 Mathlib.Data.Multiset.Bind
  {α : Type u_1} {β : Type v} (b : β) (s : Multiset α) (t : Multiset β) : s ×ˢ (b ::ₘ t) = Multiset.map (fun a => (a, b)) s + s ×ˢ t
• Finset.prod.eq_1 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
  {α : Type u_3} {β : Type u_4} [CommMonoid β] (s : Finset α) (f : α → β) : s.prod f = (Multiset.map f s.val).prod
• Finset.sum.eq_1 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
  {α : Type u_3} {β : Type u_4} [AddCommMonoid β] (s : Finset α) (f : α → β) : s.sum f = (Multiset.map f s.val).sum
• Finset.prod_eq_multiset_prod 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
  {α : Type u_3} {β : Type u_4} [CommMonoid β] (s : Finset α) (f : α → β) : ∏ x ∈ s, f x = (Multiset.map f s.val).prod
• Finset.prod_map_val 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
  {α : Type u_3} {β : Type u_4} [CommMonoid β] (s : Finset α) (f : α → β) : (Multiset.map f s.val).prod = ∏ a ∈ s, f a
• Finset.sum_eq_multiset_sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
  {α : Type u_3} {β : Type u_4} [AddCommMonoid β] (s : Finset α) (f : α → β) : ∑ x ∈ s, f x = (Multiset.map f s.val).sum
• Finset.sum_map_val 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
  {α : Type u_3} {β : Type u_4} [AddCommMonoid β] (s : Finset α) (f : α → β) : (Multiset.map f s.val).sum = ∑ a ∈ s, f a
• Finset.prod_mk 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
  {α : Type u_3} {β : Type u_4} [CommMonoid β] (s : Multiset α) (hs : s.Nodup) (f : α → β) : { val := s, nodup := hs }.prod f = (Multiset.map f s).prod
• Finset.sum_mk 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
  {α : Type u_3} {β : Type u_4} [AddCommMonoid β] (s : Multiset α) (hs : s.Nodup) (f : α → β) : { val := s, nodup := hs }.sum f = (Multiset.map f s).sum
• ofAdd_multiset_prod 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
  {α : Type u_3} [AddCommMonoid α] (s : Multiset α) : Multiplicative.ofAdd s.sum = (Multiset.map (⇑Multiplicative.ofAdd) s).prod
• ofMul_multiset_prod 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
  {α : Type u_3} [CommMonoid α] (s : Multiset α) : Additive.ofMul s.prod = (Multiset.map (⇑Additive.ofMul) s).sum
• toAdd_multiset_sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
  {α : Type u_3} [AddCommMonoid α] (s : Multiset (Multiplicative α)) : Multiplicative.toAdd s.prod = (Multiset.map (⇑Multiplicative.toAdd) s).sum
• toMul_multiset_sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
  {α : Type u_3} [CommMonoid α] (s : Multiset (Additive α)) : Additive.toMul s.sum = (Multiset.map (⇑Additive.toMul) s).prod
• Finset.image.eq_1 📋 Mathlib.Data.Finset.Card
  {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : α → β) (s : Finset α) : Finset.image f s = (Multiset.map f s.val).toFinset
• Finset.map.eq_1 📋 Mathlib.Data.Finset.Fold
  {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Finset α) : Finset.map f s = { val := Multiset.map (⇑f) s.val, nodup := ⋯ }
• Finset.fold.eq_1 📋 Mathlib.Data.Finset.Fold
  {α : Type u_1} {β : Type u_2} (op : β → β → β) [hc : Std.Commutative op] [ha : Std.Associative op] (b : β) (f : α → β) (s : Finset α) : Finset.fold op b f s = Multiset.fold op b (Multiset.map f s.val)
• Multiset.disjSum_zero 📋 Mathlib.Data.Multiset.Sum
  {α : Type u_1} {β : Type u_2} (s : Multiset α) : s.disjSum 0 = Multiset.map Sum.inl s
• Multiset.zero_disjSum 📋 Mathlib.Data.Multiset.Sum
  {α : Type u_1} {β : Type u_2} (t : Multiset β) : Multiset.disjSum 0 t = Multiset.map Sum.inr t
• Multiset.disjSum.eq_1 📋 Mathlib.Data.Multiset.Sum
  {α : Type u_1} {β : Type u_2} (s : Multiset α) (t : Multiset β) : s.disjSum t = Multiset.map Sum.inl s + Multiset.map Sum.inr t
• Multiset.map_disjSum 📋 Mathlib.Data.Multiset.Sum
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Multiset α} {t : Multiset β} (f : α ⊕ β → γ) : Multiset.map f (s.disjSum t) = Multiset.map (fun x => f (Sum.inl x)) s + Multiset.map (fun x => f (Sum.inr x)) t
• Finset.prod_multiset_map_count 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
  {ι : Type u_1} [DecidableEq ι] (s : Multiset ι) {M : Type u_5} [CommMonoid M] (f : ι → M) : (Multiset.map f s).prod = ∏ m ∈ s.toFinset, f m ^ Multiset.count m s
• Finset.sum_multiset_map_count 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
  {ι : Type u_1} [DecidableEq ι] (s : Multiset ι) {M : Type u_5} [AddCommMonoid M] (f : ι → M) : (Multiset.map f s).sum = ∑ m ∈ s.toFinset, Multiset.count m s • f m
• Fin.univ_val_map 📋 Mathlib.Data.Fintype.Basic
  {α : Type u_1} {n : ℕ} (f : Fin n → α) : Multiset.map f Finset.univ.val = ↑(List.ofFn f)
• Multiset.bijective_iff_map_univ_eq_univ 📋 Mathlib.Data.Fintype.Basic
  {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f : α → β) : Function.Bijective f ↔ Multiset.map f Finset.univ.val = Finset.univ.val
• Multiset.map_univ_val_equiv 📋 Mathlib.Data.Fintype.Basic
  {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (e : α ≃ β) : Multiset.map (⇑e) Finset.univ.val = Finset.univ.val
• Finset.noncommProd_lemma 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [Monoid β] (s : Finset α) (f : α → β) (comm : (↑s).Pairwise (Function.onFun Commute f)) : {x | x ∈ Multiset.map f s.val}.Pairwise Commute
• Finset.noncommSum_lemma 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [AddMonoid β] (s : Finset α) (f : α → β) (comm : (↑s).Pairwise (Function.onFun AddCommute f)) : {x | x ∈ Multiset.map f s.val}.Pairwise AddCommute
• Finset.noncommProd.eq_1 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [Monoid β] (s : Finset α) (f : α → β) (comm : (↑s).Pairwise (Function.onFun Commute f)) : s.noncommProd f comm = (Multiset.map f s.val).noncommProd ⋯
• Finset.noncommSum.eq_1 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [AddMonoid β] (s : Finset α) (f : α → β) (comm : (↑s).Pairwise (Function.onFun AddCommute f)) : s.noncommSum f comm = (Multiset.map f s.val).noncommSum ⋯
• Multiset.map_noncommProd_aux 📋 Mathlib.Data.Finset.NoncommProd
  {F : Type u_1} {α : Type u_3} {β : Type u_4} [Monoid α] [Monoid β] [FunLike F α β] [MulHomClass F α β] (s : Multiset α) (comm : {x | x ∈ s}.Pairwise Commute) (f : F) : {x | x ∈ Multiset.map (⇑f) s}.Pairwise Commute
• Multiset.map_noncommSum_aux 📋 Mathlib.Data.Finset.NoncommProd
  {F : Type u_1} {α : Type u_3} {β : Type u_4} [AddMonoid α] [AddMonoid β] [FunLike F α β] [AddHomClass F α β] (s : Multiset α) (comm : {x | x ∈ s}.Pairwise AddCommute) (f : F) : {x | x ∈ Multiset.map (⇑f) s}.Pairwise AddCommute
• Multiset.map_noncommProd 📋 Mathlib.Data.Finset.NoncommProd
  {F : Type u_1} {α : Type u_3} {β : Type u_4} [Monoid α] [Monoid β] [FunLike F α β] [MonoidHomClass F α β] (s : Multiset α) (comm : {x | x ∈ s}.Pairwise Commute) (f : F) : f (s.noncommProd comm) = (Multiset.map (⇑f) s).noncommProd ⋯

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 19971e9 serving mathlib revision bce1d65