Loogle!

Result

Found 8 declarations mentioning Multiset.sum and LT.lt.

• Multiset.sum_lt_sum_of_nonempty 📋 Mathlib.Algebra.Order.BigOperators.Group.Multiset
  {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s : Multiset ι} {f g : ι → α} (hs : s ≠ ∅) (hfg : ∀ i ∈ s, f i < g i) : (Multiset.map f s).sum < (Multiset.map g s).sum
• Multiset.sum_lt_sum 📋 Mathlib.Algebra.Order.BigOperators.Group.Multiset
  {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s : Multiset ι} {f g : ι → α} (hle : ∀ i ∈ s, f i ≤ g i) (hlt : ∃ i ∈ s, f i < g i) : (Multiset.map f s).sum < (Multiset.map g s).sum
• Polynomial.multiset_prod_X_sub_C_coeff_card_pred 📋 Mathlib.Algebra.Polynomial.BigOperators
  {R : Type u} [CommRing R] (t : Multiset R) (ht : 0 < t.card) : (Multiset.map (fun x => Polynomial.X - Polynomial.C x) t).prod.coeff (t.card - 1) = -t.sum
• Nat.Partition.mk 📋 Mathlib.Combinatorics.Enumerative.Partition.Basic
  {n : ℕ} (parts : Multiset ℕ) (parts_pos : ∀ {i : ℕ}, i ∈ parts → 0 < i) (parts_sum : parts.sum = n) : n.Partition
• Nat.Partition.mk.injEq 📋 Mathlib.Combinatorics.Enumerative.Partition.Basic
  {n : ℕ} (parts : Multiset ℕ) (parts_pos : ∀ {i : ℕ}, i ∈ parts → 0 < i) (parts_sum : parts.sum = n) (parts✝ : Multiset ℕ) (parts_pos✝ : ∀ {i : ℕ}, i ∈ parts✝ → 0 < i) (parts_sum✝ : parts✝.sum = n) : ({ parts := parts, parts_pos := parts_pos, parts_sum := parts_sum } = { parts := parts✝, parts_pos := parts_pos✝, parts_sum := parts_sum✝ }) = (parts = parts✝)
• Nat.Partition.mk.sizeOf_spec 📋 Mathlib.Combinatorics.Enumerative.Partition.Basic
  {n : ℕ} (parts : Multiset ℕ) (parts_pos : ∀ {i : ℕ}, i ∈ parts → 0 < i) (parts_sum : parts.sum = n) : sizeOf { parts := parts, parts_pos := parts_pos, parts_sum := parts_sum } = 1 + sizeOf parts + sizeOf parts_sum
• Nat.Partition.mk.congr_simp 📋 Mathlib.Combinatorics.Enumerative.Partition.Basic
  {n : ℕ} (parts parts✝ : Multiset ℕ) (e_parts : parts = parts✝) (parts_pos : ∀ {i : ℕ}, i ∈ parts → 0 < i) (parts_sum : parts.sum = n) : { parts := parts, parts_pos := parts_pos, parts_sum := parts_sum } = { parts := parts✝, parts_pos := ⋯, parts_sum := ⋯ }
• multisetProd_apply_eq_zero' 📋 Mathlib.Algebra.DirectSum.Internal
  {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [AddCommMonoid ι] [LinearOrder ι] [IsOrderedAddMonoid ι] [DecidableEq ι] [CanonicallyOrderedAdd ι] [CommSemiring R] [SetLike σ R] [AddSubmonoidClass σ R] {A : ι → σ} [SetLike.GradedMonoid A] {s : Multiset ((DirectSum ι fun i => ↥(A i)) × ι)} (hs : ∀ xn ∈ s, ∀ k < xn.2, xn.1 k = 0) ⦃n : ι⦄ (hn : n < (Multiset.map Prod.snd s).sum) : (Multiset.map Prod.fst s).prod n = 0

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 6ff4759 serving mathlib revision f91c049