Loogle!

Result

Found 832 declarations mentioning Finset.range. Of these, only the first 200 are shown.

Finset.range 📋 Mathlib.Data.Finset.Range
(n : ℕ) : Finset ℕ
Finset.range_val 📋 Mathlib.Data.Finset.Range
(n : ℕ) : (Finset.range n).val = Multiset.range n
Finset.range_mono 📋 Mathlib.Data.Finset.Range
: Monotone Finset.range
Finset.strictMono_range 📋 Mathlib.Data.Finset.Range
: StrictMono Finset.range
Multiset.toFinset_range 📋 Mathlib.Data.Finset.Range
(n : ℕ) : (Multiset.range n).toFinset = Finset.range n
Finset.Aesop.range_nonempty 📋 Mathlib.Data.Finset.Range
{n : ℕ} : n ≠ 0 → (Finset.range n).Nonempty
Finset.nonempty_range_iff 📋 Mathlib.Data.Finset.Range
{n : ℕ} : (Finset.range n).Nonempty ↔ n ≠ 0
Finset.range_nontrivial 📋 Mathlib.Data.Finset.Range
{n : ℕ} (hn : 1 < n) : (Finset.range n).Nontrivial
Finset.range_zero 📋 Mathlib.Data.Finset.Range
: Finset.range 0 = ∅
Finset.notMem_range_self 📋 Mathlib.Data.Finset.Range
{n : ℕ} : n ∉ Finset.range n
Finset.coe_range 📋 Mathlib.Data.Finset.Range
(n : ℕ) : ↑(Finset.range n) = Set.Iio n
Finset.nonempty_range_add_one 📋 Mathlib.Data.Finset.Range
{n : ℕ} : (Finset.range (n + 1)).Nonempty
Finset.exists_nat_subset_range 📋 Mathlib.Data.Finset.Range
(s : Finset ℕ) : ∃ n, s ⊆ Finset.range n
notMemRangeEquiv 📋 Mathlib.Data.Finset.Range
(k : ℕ) : { n // n ∉ Finset.range k } ≃ ℕ
Finset.mem_range_le 📋 Mathlib.Data.Finset.Range
{n x : ℕ} (hx : x ∈ Finset.range n) : x ≤ n
Finset.range_eq_empty_iff 📋 Mathlib.Data.Finset.Range
{n : ℕ} : Finset.range n = ∅ ↔ n = 0
Finset.range_one 📋 Mathlib.Data.Finset.Range
: Finset.range 1 = {0}
Finset.mem_range 📋 Mathlib.Data.Finset.Range
{n m : ℕ} : m ∈ Finset.range n ↔ m < n
Finset.mem_range_succ_iff 📋 Mathlib.Data.Finset.Range
{a b : ℕ} : a ∈ Finset.range b.succ ↔ a ≤ b
Finset.range_subset_range 📋 Mathlib.Data.Finset.Range
{n m : ℕ} : Finset.range n ⊆ Finset.range m ↔ n ≤ m
Finset.self_mem_range_succ 📋 Mathlib.Data.Finset.Range
(n : ℕ) : n ∈ Finset.range (n + 1)
Finset.range_add_one 📋 Mathlib.Data.Finset.Range
{n : ℕ} : Finset.range (n + 1) = insert n (Finset.range n)
Finset.mem_range_sub_ne_zero 📋 Mathlib.Data.Finset.Range
{n x : ℕ} (hx : x ∈ Finset.range n) : n - x ≠ 0
Finset.range_subset 📋 Mathlib.Data.Finset.Range
{n : ℕ} {s : Finset ℕ} : Finset.range n ⊆ s ↔ ∀ x < n, x ∈ s
Finset.subset_range 📋 Mathlib.Data.Finset.Range
{s : Finset ℕ} {n : ℕ} : s ⊆ Finset.range n ↔ ∀ x ∈ s, x < n
coe_notMemRangeEquiv_symm 📋 Mathlib.Data.Finset.Range
(k : ℕ) : ⇑(notMemRangeEquiv k).symm = fun j => ⟨j + k, ⋯⟩
coe_notMemRangeEquiv 📋 Mathlib.Data.Finset.Range
(k : ℕ) : ⇑(notMemRangeEquiv k) = fun i => ↑i - k
Finset.range_inter_range 📋 Mathlib.Data.Finset.Basic
(m n : ℕ) : Finset.range m ∩ Finset.range n = Finset.range (min m n)
Finset.range_union_range 📋 Mathlib.Data.Finset.Basic
(m n : ℕ) : Finset.range m ∪ Finset.range n = Finset.range (max m n)
Finset.range_filter_eq 📋 Mathlib.Data.Finset.Basic
{n m : ℕ} : {x ∈ Finset.range n | x = m} = if m < n then {m} else ∅
Finset.range_sdiff_zero 📋 Mathlib.Data.Finset.Image
{n : ℕ} : Finset.range (n + 1) \ {0} = Finset.image Nat.succ (Finset.range n)
Finset.range_add_one' 📋 Mathlib.Data.Finset.Image
(n : ℕ) : Finset.range (n + 1) = insert 0 (Finset.map { toFun := fun i => i + 1, inj' := ⋯ } (Finset.range n))
Finset.mem_range_iff_mem_finset_range_of_mod_eq' 📋 Mathlib.Data.Finset.Image
{α : Type u_1} [DecidableEq α] {f : ℕ → α} {a : α} {n : ℕ} (hn : 0 < n) (h : ∀ (i : ℕ), f (i % n) = f i) : a ∈ Set.range f ↔ a ∈ Finset.image (fun i => f i) (Finset.range n)
Finset.mem_range_iff_mem_finset_range_of_mod_eq 📋 Mathlib.Data.Finset.Image
{α : Type u_1} [DecidableEq α] {f : ℤ → α} {a : α} {n : ℕ} (hn : 0 < n) (h : ∀ (i : ℤ), f (i % ↑n) = f i) : a ∈ Set.range f ↔ a ∈ Finset.image (fun i => f ↑i) (Finset.range n)
Finset.card_range 📋 Mathlib.Data.Finset.Card
(n : ℕ) : (Finset.range n).card = n
Finset.subset_range_sup_succ 📋 Mathlib.Data.Finset.Lattice.Fold
(s : Finset ℕ) : s ⊆ Finset.range (s.sup id).succ
Finset.powerset_card_biUnion 📋 Mathlib.Data.Finset.Powerset
{α : Type u_1} [DecidableEq (Finset α)] (s : Finset α) : s.powerset = (Finset.range (s.card + 1)).biUnion fun i => Finset.powersetCard i s
Finset.powerset_card_disjiUnion 📋 Mathlib.Data.Finset.Powerset
{α : Type u_1} (s : Finset α) : s.powerset = (Finset.range (s.card + 1)).disjiUnion (fun i => Finset.powersetCard i s) ⋯
List.toFinset_range 📋 Mathlib.Order.Interval.Finset.Nat
(a : ℕ) : (List.range a).toFinset = Finset.range a
Nat.Iio_eq_range 📋 Mathlib.Order.Interval.Finset.Nat
(a : ℕ) : Finset.Iio a = Finset.range a
Finset.range_eq_Ico 📋 Mathlib.Order.Interval.Finset.Nat
(a : ℕ) : Finset.range a = Finset.Ico 0 a
Nat.Ico_zero_eq_range 📋 Mathlib.Order.Interval.Finset.Nat
(a : ℕ) : Finset.Ico 0 a = Finset.range a
Nat.range_succ_eq_Iic 📋 Mathlib.Order.Interval.Finset.Nat
(n : ℕ) : Finset.range (n + 1) = Finset.Iic n
Nat.range_succ_eq_Icc_zero 📋 Mathlib.Order.Interval.Finset.Nat
(n : ℕ) : Finset.range (n + 1) = Finset.Icc 0 n
Finset.range_image_pred_top_sub 📋 Mathlib.Order.Interval.Finset.Nat
(n : ℕ) : Finset.image (fun j => n - 1 - j) (Finset.range n) = Finset.range n
Nat.image_Ico_mod 📋 Mathlib.Order.Interval.Finset.Nat
(n a : ℕ) : Finset.image (fun x => x % a) (Finset.Ico n (n + a)) = Finset.range a
Nat.range_eq_Icc_zero_sub_one 📋 Mathlib.Order.Interval.Finset.Nat
(n : ℕ) (hn : n ≠ 0) : Finset.range n = Finset.Icc 0 (n - 1)
Finset.range_add_eq_union 📋 Mathlib.Order.Interval.Finset.Nat
(a b : ℕ) : Finset.range (a + b) = Finset.range a ∪ Finset.map (addLeftEmbedding a) (Finset.range b)
Finset.prod_range_zero 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{M : Type u_3} [CommMonoid M] (f : ℕ → M) : ∏ k ∈ Finset.range 0, f k = 1
Finset.sum_range_zero 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{M : Type u_3} [AddCommMonoid M] (f : ℕ → M) : ∑ k ∈ Finset.range 0, f k = 0
Finset.prod_range_one 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [CommMonoid M] (f : ℕ → M) : ∏ k ∈ Finset.range 1, f k = f 0
Finset.sum_range_one 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [AddCommMonoid M] (f : ℕ → M) : ∑ k ∈ Finset.range 1, f k = f 0
Finset.nsmul_eq_sum_const 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [AddCommMonoid M] (b : M) (n : ℕ) : n • b = ∑ _k ∈ Finset.range n, b
Finset.pow_eq_prod_const 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [CommMonoid M] (b : M) (n : ℕ) : b ^ n = ∏ _k ∈ Finset.range n, b
Finset.prod_range_succ 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [CommMonoid M] (f : ℕ → M) (n : ℕ) : ∏ x ∈ Finset.range (n + 1), f x = (∏ x ∈ Finset.range n, f x) * f n
Finset.prod_range_succ_comm 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [CommMonoid M] (f : ℕ → M) (n : ℕ) : ∏ x ∈ Finset.range (n + 1), f x = f n * ∏ x ∈ Finset.range n, f x
Finset.sum_range_succ 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [AddCommMonoid M] (f : ℕ → M) (n : ℕ) : ∑ x ∈ Finset.range (n + 1), f x = ∑ x ∈ Finset.range n, f x + f n
Finset.sum_range_succ_comm 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [AddCommMonoid M] (f : ℕ → M) (n : ℕ) : ∑ x ∈ Finset.range (n + 1), f x = f n + ∑ x ∈ Finset.range n, f x
Finset.eventually_constant_prod 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [CommMonoid M] {u : ℕ → M} {N : ℕ} (hu : ∀ n ≥ N, u n = 1) {n : ℕ} (hn : N ≤ n) : ∏ k ∈ Finset.range n, u k = ∏ k ∈ Finset.range N, u k
Finset.eventually_constant_sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [AddCommMonoid M] {u : ℕ → M} {N : ℕ} (hu : ∀ n ≥ N, u n = 0) {n : ℕ} (hn : N ≤ n) : ∑ k ∈ Finset.range n, u k = ∑ k ∈ Finset.range N, u k
Finset.prod_flip 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [CommMonoid M] {n : ℕ} (f : ℕ → M) : ∏ r ∈ Finset.range (n + 1), f (n - r) = ∏ k ∈ Finset.range (n + 1), f k
Finset.sum_flip 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [AddCommMonoid M] {n : ℕ} (f : ℕ → M) : ∑ r ∈ Finset.range (n + 1), f (n - r) = ∑ k ∈ Finset.range (n + 1), f k
Finset.prod_range_add 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [CommMonoid M] (f : ℕ → M) (n m : ℕ) : ∏ x ∈ Finset.range (n + m), f x = (∏ x ∈ Finset.range n, f x) * ∏ x ∈ Finset.range m, f (n + x)
Finset.prod_range_div 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{G : Type u_3} [CommGroup G] (f : ℕ → G) (n : ℕ) : ∏ i ∈ Finset.range n, f (i + 1) / f i = f n / f 0
Finset.prod_range_div' 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{G : Type u_3} [CommGroup G] (f : ℕ → G) (n : ℕ) : ∏ i ∈ Finset.range n, f i / f (i + 1) = f 0 / f n
Finset.sum_range_add 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [AddCommMonoid M] (f : ℕ → M) (n m : ℕ) : ∑ x ∈ Finset.range (n + m), f x = ∑ x ∈ Finset.range n, f x + ∑ x ∈ Finset.range m, f (n + x)
Finset.sum_range_sub 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{G : Type u_3} [AddCommGroup G] (f : ℕ → G) (n : ℕ) : ∑ i ∈ Finset.range n, (f (i + 1) - f i) = f n - f 0
Finset.sum_range_sub' 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{G : Type u_3} [AddCommGroup G] (f : ℕ → G) (n : ℕ) : ∑ i ∈ Finset.range n, (f i - f (i + 1)) = f 0 - f n
Finset.prod_range_add_div_prod_range 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{G : Type u_3} [CommGroup G] (f : ℕ → G) (n m : ℕ) : (∏ k ∈ Finset.range (n + m), f k) / ∏ k ∈ Finset.range n, f k = ∏ k ∈ Finset.range m, f (n + k)
Finset.prod_range_succ' 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [CommMonoid M] (f : ℕ → M) (n : ℕ) : ∏ k ∈ Finset.range (n + 1), f k = (∏ k ∈ Finset.range n, f (k + 1)) * f 0
Finset.sum_range_add_sub_sum_range 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{G : Type u_3} [AddCommGroup G] (f : ℕ → G) (n m : ℕ) : ∑ k ∈ Finset.range (n + m), f k - ∑ k ∈ Finset.range n, f k = ∑ k ∈ Finset.range m, f (n + k)
Finset.sum_range_succ' 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [AddCommMonoid M] (f : ℕ → M) (n : ℕ) : ∑ k ∈ Finset.range (n + 1), f k = ∑ k ∈ Finset.range n, f (k + 1) + f 0
Finset.eq_prod_range_div 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{G : Type u_3} [CommGroup G] (f : ℕ → G) (n : ℕ) : f n = f 0 * ∏ i ∈ Finset.range n, f (i + 1) / f i
Finset.eq_sum_range_sub 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{G : Type u_3} [AddCommGroup G] (f : ℕ → G) (n : ℕ) : f n = f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i)
Finset.eq_prod_range_div' 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{G : Type u_3} [CommGroup G] (f : ℕ → G) (n : ℕ) : f n = ∏ i ∈ Finset.range (n + 1), if i = 0 then f 0 else f i / f (i - 1)
Finset.eq_sum_range_sub' 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{G : Type u_3} [AddCommGroup G] (f : ℕ → G) (n : ℕ) : f n = ∑ i ∈ Finset.range (n + 1), if i = 0 then f 0 else f i - f (i - 1)
Finset.prod_range_induction 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [CommMonoid M] (f s : ℕ → M) (base : s 0 = 1) (n : ℕ) (step : ∀ k < n, s (k + 1) = s k * f k) : ∏ k ∈ Finset.range n, f k = s n
Finset.sum_range_induction 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [AddCommMonoid M] (f s : ℕ → M) (base : s 0 = 0) (n : ℕ) (step : ∀ k < n, s (k + 1) = s k + f k) : ∑ k ∈ Finset.range n, f k = s n
Finset.sum_range_tsub 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [AddCommMonoid M] [PartialOrder M] [Sub M] [OrderedSub M] [AddLeftMono M] [AddLeftReflectLE M] [ExistsAddOfLE M] {f : ℕ → M} (h : Monotone f) (n : ℕ) : ∑ i ∈ Finset.range n, (f (i + 1) - f i) = f n - f 0
Fin.prod_univ_eq_prod_range 📋 Mathlib.Data.Fintype.BigOperators
{α : Type u_1} [CommMonoid α] (f : ℕ → α) (n : ℕ) : ∏ i, f ↑i = ∏ i ∈ Finset.range n, f i
Fin.sum_univ_eq_sum_range 📋 Mathlib.Data.Fintype.BigOperators
{α : Type u_1} [AddCommMonoid α] (f : ℕ → α) (n : ℕ) : ∑ i, f ↑i = ∑ i ∈ Finset.range n, f i
Finset.prod_fin_eq_prod_range 📋 Mathlib.Data.Fintype.BigOperators
{β : Type u_2} [CommMonoid β] {n : ℕ} (c : Fin n → β) : ∏ i, c i = ∏ i ∈ Finset.range n, if h : i < n then c ⟨i, h⟩ else 1
Finset.sum_fin_eq_sum_range 📋 Mathlib.Data.Fintype.BigOperators
{β : Type u_2} [AddCommMonoid β] {n : ℕ} (c : Fin n → β) : ∑ i, c i = ∑ i ∈ Finset.range n, if h : i < n then c ⟨i, h⟩ else 0
Finset.prod_range_natCast_sub 📋 Mathlib.Algebra.BigOperators.Ring.Finset
{R : Type u_4} [CommRing R] (n k : ℕ) : ∏ i ∈ Finset.range k, (↑n - ↑i) = ↑(∏ i ∈ Finset.range k, (n - i))
Finset.sum_range_succ_mul_sum_range_succ 📋 Mathlib.Algebra.BigOperators.Ring.Finset
{R : Type u_4} [NonUnitalNonAssocSemiring R] (m n : ℕ) (f g : ℕ → R) : (∑ i ∈ Finset.range (m + 1), f i) * ∑ i ∈ Finset.range (n + 1), g i = (∑ i ∈ Finset.range m, f i) * ∑ i ∈ Finset.range n, g i + f m * ∑ i ∈ Finset.range n, g i + (∑ i ∈ Finset.range m, f i) * g n + f m * g n
Multiset.sup_powerset_len 📋 Mathlib.Algebra.Order.BigOperators.Group.Finset
{α : Type u_2} [DecidableEq α] (x : Multiset α) : ((Finset.range (x.card + 1)).sup fun k => Multiset.powersetCard k x) = x.powerset
Finset.image_fin_univ 📋 Mathlib.Data.Fintype.Fin
{n : ℕ} : Finset.image Fin.val Finset.univ = Finset.range n
Finset.sup_fin_univ 📋 Mathlib.Data.Fintype.Fin
{α : Type u_1} [SemilatticeSup α] [OrderBot α] {n : ℕ} (f : ℕ → α) : (Finset.univ.sup fun n_1 => f ↑n_1) = (Finset.range n).sup f
Finset.prod_range 📋 Mathlib.Algebra.BigOperators.Fin
{M : Type u_2} [CommMonoid M] {n : ℕ} (f : ℕ → M) : ∏ i ∈ Finset.range n, f i = ∏ i, f ↑i
Finset.sum_range 📋 Mathlib.Algebra.BigOperators.Fin
{M : Type u_2} [AddCommMonoid M] {n : ℕ} (f : ℕ → M) : ∑ i ∈ Finset.range n, f i = ∑ i, f ↑i
partialSups_eq_sup'_range 📋 Mathlib.Order.PartialSups
{α : Type u_1} [SemilatticeSup α] (f : ℕ → α) (n : ℕ) : (partialSups f) n = (Finset.range (n + 1)).sup' ⋯ f
partialSups_eq_sup_range 📋 Mathlib.Order.PartialSups
{α : Type u_1} [SemilatticeSup α] [OrderBot α] (f : ℕ → α) (n : ℕ) : (partialSups f) n = (Finset.range (n + 1)).sup f
partialSups_eq_sUnion_image 📋 Mathlib.Order.PartialSups
{α : Type u_1} (s : ℕ → Set α) (n : ℕ) : (partialSups s) n = ⋃₀ ↑(Finset.image s (Finset.range (n + 1)))
partialSups_eq_biUnion_range 📋 Mathlib.Order.PartialSups
{α : Type u_1} (s : ℕ → Set α) (n : ℕ) : (partialSups s) n = ⋃ i ∈ Finset.range (n + 1), s i
orderIsoRangeOfLinearSuccPredArch 📋 Mathlib.Order.SuccPred.LinearLocallyFinite
{ι : Type u_1} [LinearOrder ι] [SuccOrder ι] [PredOrder ι] [IsSuccArchimedean ι] [OrderBot ι] [OrderTop ι] : ι ≃o ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
biUnion_range_succ_disjointed 📋 Mathlib.Order.Disjointed
{α : Type u_3} (f : ℕ → Set α) (n : ℕ) : ⋃ i ∈ Finset.range (n + 1), disjointed f i = (partialSups f) n
Finset.prod_eq_prod_range_sdiff 📋 Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
{α : Type u_3} {β : Type u_4} [DecidableEq α] [CommMonoid β] (s : ℕ → Finset α) (hs : Monotone s) (g : α → β) (n : ℕ) : ∏ i ∈ s n, g i = (∏ i ∈ s 0, g i) * ∏ i ∈ Finset.range n, ∏ j ∈ s (i + 1) \ s i, g j
Finset.sum_eq_sum_range_sdiff 📋 Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
{α : Type u_3} {β : Type u_4} [DecidableEq α] [AddCommMonoid β] (s : ℕ → Finset α) (hs : Monotone s) (g : α → β) (n : ℕ) : ∑ i ∈ s n, g i = ∑ i ∈ s 0, g i + ∑ i ∈ Finset.range n, ∑ j ∈ s (i + 1) \ s i, g j
Finset.sum_range_id 📋 Mathlib.Algebra.BigOperators.Intervals
(n : ℕ) : ∑ i ∈ Finset.range n, i = n * (n - 1) / 2
Finset.sum_range_id_mul_two 📋 Mathlib.Algebra.BigOperators.Intervals
(n : ℕ) : (∑ i ∈ Finset.range n, i) * 2 = n * (n - 1)
Finset.prod_range_reflect 📋 Mathlib.Algebra.BigOperators.Intervals
{M : Type u_3} [CommMonoid M] (f : ℕ → M) (n : ℕ) : ∏ j ∈ Finset.range n, f (n - 1 - j) = ∏ j ∈ Finset.range n, f j
Finset.sum_range_reflect 📋 Mathlib.Algebra.BigOperators.Intervals
{M : Type u_3} [AddCommMonoid M] (f : ℕ → M) (n : ℕ) : ∑ j ∈ Finset.range n, f (n - 1 - j) = ∑ j ∈ Finset.range n, f j
Finset.prod_Ico_eq_prod_range 📋 Mathlib.Algebra.BigOperators.Intervals
{M : Type u_3} [CommMonoid M] (f : ℕ → M) (m n : ℕ) : ∏ k ∈ Finset.Ico m n, f k = ∏ k ∈ Finset.range (n - m), f (m + k)
Finset.sum_Ico_eq_sum_range 📋 Mathlib.Algebra.BigOperators.Intervals
{M : Type u_3} [AddCommMonoid M] (f : ℕ → M) (m n : ℕ) : ∑ k ∈ Finset.Ico m n, f k = ∑ k ∈ Finset.range (n - m), f (m + k)
Finset.prod_range_succ_div_prod 📋 Mathlib.Algebra.BigOperators.Intervals
{M : Type u_4} (f : ℕ → M) {n : ℕ} [CommGroup M] : (∏ i ∈ Finset.range (n + 1), f i) / ∏ i ∈ Finset.range n, f i = f n
Finset.prod_range_succ_div_top 📋 Mathlib.Algebra.BigOperators.Intervals
{M : Type u_4} (f : ℕ → M) {n : ℕ} [CommGroup M] : (∏ i ∈ Finset.range (n + 1), f i) / f n = ∏ i ∈ Finset.range n, f i
Finset.sum_range_succ_sub_sum 📋 Mathlib.Algebra.BigOperators.Intervals
{M : Type u_4} (f : ℕ → M) {n : ℕ} [AddCommGroup M] : ∑ i ∈ Finset.range (n + 1), f i - ∑ i ∈ Finset.range n, f i = f n
Finset.sum_range_succ_sub_top 📋 Mathlib.Algebra.BigOperators.Intervals
{M : Type u_4} (f : ℕ → M) {n : ℕ} [AddCommGroup M] : ∑ i ∈ Finset.range (n + 1), f i - f n = ∑ i ∈ Finset.range n, f i
Finset.prod_range_mul_prod_Ico 📋 Mathlib.Algebra.BigOperators.Intervals
{M : Type u_3} [CommMonoid M] (f : ℕ → M) {m n : ℕ} (h : m ≤ n) : (∏ k ∈ Finset.range m, f k) * ∏ k ∈ Finset.Ico m n, f k = ∏ k ∈ Finset.range n, f k
Finset.sum_range_add_sum_Ico 📋 Mathlib.Algebra.BigOperators.Intervals
{M : Type u_3} [AddCommMonoid M] (f : ℕ → M) {m n : ℕ} (h : m ≤ n) : ∑ k ∈ Finset.range m, f k + ∑ k ∈ Finset.Ico m n, f k = ∑ k ∈ Finset.range n, f k
Finset.prod_Ico_eq_div 📋 Mathlib.Algebra.BigOperators.Intervals
{δ : Type u_4} [CommGroup δ] (f : ℕ → δ) {m n : ℕ} (h : m ≤ n) : ∏ k ∈ Finset.Ico m n, f k = (∏ k ∈ Finset.range n, f k) / ∏ k ∈ Finset.range m, f k
Finset.prod_range_eq_mul_Ico 📋 Mathlib.Algebra.BigOperators.Intervals
{M : Type u_3} [CommMonoid M] (f : ℕ → M) {n : ℕ} (hn : 0 < n) : ∏ x ∈ Finset.range n, f x = f 0 * ∏ x ∈ Finset.Ico 1 n, f x
Finset.sum_Ico_eq_sub 📋 Mathlib.Algebra.BigOperators.Intervals
{δ : Type u_4} [AddCommGroup δ] (f : ℕ → δ) {m n : ℕ} (h : m ≤ n) : ∑ k ∈ Finset.Ico m n, f k = ∑ k ∈ Finset.range n, f k - ∑ k ∈ Finset.range m, f k
Finset.sum_range_eq_add_Ico 📋 Mathlib.Algebra.BigOperators.Intervals
{M : Type u_3} [AddCommMonoid M] (f : ℕ → M) {n : ℕ} (hn : 0 < n) : ∑ x ∈ Finset.range n, f x = f 0 + ∑ x ∈ Finset.Ico 1 n, f x
Finset.prod_range_div_prod_range 📋 Mathlib.Algebra.BigOperators.Intervals
{G : Type u_4} [CommGroup G] {f : ℕ → G} {n m : ℕ} (hnm : n ≤ m) : (∏ k ∈ Finset.range m, f k) / ∏ k ∈ Finset.range n, f k = ∏ k ∈ Finset.range m with n ≤ k, f k
Finset.sum_range_sub_sum_range 📋 Mathlib.Algebra.BigOperators.Intervals
{G : Type u_4} [AddCommGroup G] {f : ℕ → G} {n m : ℕ} (hnm : n ≤ m) : ∑ k ∈ Finset.range m, f k - ∑ k ∈ Finset.range n, f k = ∑ k ∈ Finset.range m with n ≤ k, f k
Finset.prod_range_diag_flip 📋 Mathlib.Algebra.BigOperators.Intervals
{M : Type u_3} [CommMonoid M] (n : ℕ) (f : ℕ → ℕ → M) : ∏ m ∈ Finset.range n, ∏ k ∈ Finset.range (m + 1), f k (m - k) = ∏ m ∈ Finset.range n, ∏ k ∈ Finset.range (n - m), f m k
Finset.sum_range_diag_flip 📋 Mathlib.Algebra.BigOperators.Intervals
{M : Type u_3} [AddCommMonoid M] (n : ℕ) (f : ℕ → ℕ → M) : ∑ m ∈ Finset.range n, ∑ k ∈ Finset.range (m + 1), f k (m - k) = ∑ m ∈ Finset.range n, ∑ k ∈ Finset.range (n - m), f m k
Finset.prod_Ico_eq_mul_inv 📋 Mathlib.Algebra.BigOperators.Intervals
{δ : Type u_4} [CommGroup δ] (f : ℕ → δ) {m n : ℕ} (h : m ≤ n) : ∏ k ∈ Finset.Ico m n, f k = (∏ k ∈ Finset.range n, f k) * (∏ k ∈ Finset.range m, f k)⁻¹
Finset.sum_Ico_eq_add_neg 📋 Mathlib.Algebra.BigOperators.Intervals
{δ : Type u_4} [AddCommGroup δ] (f : ℕ → δ) {m n : ℕ} (h : m ≤ n) : ∑ k ∈ Finset.Ico m n, f k = ∑ k ∈ Finset.range n, f k + -∑ k ∈ Finset.range m, f k
Finset.Nat.antidiagonal_eq_image 📋 Mathlib.Data.Finset.NatAntidiagonal
(n : ℕ) : Finset.HasAntidiagonal.antidiagonal n = Finset.image (fun i => (i, n - i)) (Finset.range (n + 1))
Finset.Nat.antidiagonal_eq_image' 📋 Mathlib.Data.Finset.NatAntidiagonal
(n : ℕ) : Finset.HasAntidiagonal.antidiagonal n = Finset.image (fun i => (n - i, i)) (Finset.range (n + 1))
Finset.Nat.antidiagonal_eq_map 📋 Mathlib.Data.Finset.NatAntidiagonal
(n : ℕ) : Finset.HasAntidiagonal.antidiagonal n = Finset.map { toFun := fun i => (i, n - i), inj' := ⋯ } (Finset.range (n + 1))
Finset.Nat.antidiagonal_eq_map' 📋 Mathlib.Data.Finset.NatAntidiagonal
(n : ℕ) : Finset.HasAntidiagonal.antidiagonal n = Finset.map { toFun := fun i => (n - i, i), inj' := ⋯ } (Finset.range (n + 1))
Finset.Nat.prod_antidiagonal_eq_prod_range_succ_mk 📋 Mathlib.Algebra.BigOperators.NatAntidiagonal
{M : Type u_2} [CommMonoid M] (f : ℕ × ℕ → M) (n : ℕ) : ∏ ij ∈ Finset.HasAntidiagonal.antidiagonal n, f ij = ∏ k ∈ Finset.range n.succ, f (k, n - k)
Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk 📋 Mathlib.Algebra.BigOperators.NatAntidiagonal
{M : Type u_2} [AddCommMonoid M] (f : ℕ × ℕ → M) (n : ℕ) : ∑ ij ∈ Finset.HasAntidiagonal.antidiagonal n, f ij = ∑ k ∈ Finset.range n.succ, f (k, n - k)
Finset.Nat.prod_antidiagonal_eq_prod_range_succ 📋 Mathlib.Algebra.BigOperators.NatAntidiagonal
{M : Type u_2} [CommMonoid M] (f : ℕ → ℕ → M) (n : ℕ) : ∏ ij ∈ Finset.HasAntidiagonal.antidiagonal n, f ij.1 ij.2 = ∏ k ∈ Finset.range n.succ, f k (n - k)
Finset.Nat.sum_antidiagonal_eq_sum_range_succ 📋 Mathlib.Algebra.BigOperators.NatAntidiagonal
{M : Type u_2} [AddCommMonoid M] (f : ℕ → ℕ → M) (n : ℕ) : ∑ ij ∈ Finset.HasAntidiagonal.antidiagonal n, f ij.1 ij.2 = ∑ k ∈ Finset.range n.succ, f k (n - k)
Nat.sum_range_multichoose 📋 Mathlib.Data.Nat.Choose.Sum
(n k : ℕ) : ∑ i ∈ Finset.range (n + 1), k.multichoose i = (n + k).choose k
Nat.sum_range_choose 📋 Mathlib.Data.Nat.Choose.Sum
(n : ℕ) : ∑ m ∈ Finset.range (n + 1), n.choose m = 2 ^ n
Finset.sum_powerset_apply_card 📋 Mathlib.Data.Nat.Choose.Sum
{α : Type u_2} {β : Type u_3} [AddCommMonoid α] (f : ℕ → α) {x : Finset β} : ∑ m ∈ x.powerset, f m.card = ∑ m ∈ Finset.range (x.card + 1), x.card.choose m • f m
Nat.sum_range_choose_halfway 📋 Mathlib.Data.Nat.Choose.Sum
(m : ℕ) : ∑ i ∈ Finset.range (m + 1), (2 * m + 1).choose i = 4 ^ m
Int.alternating_sum_range_choose_of_ne 📋 Mathlib.Data.Nat.Choose.Sum
{n : ℕ} (h0 : n ≠ 0) : ∑ m ∈ Finset.range (n + 1), (-1) ^ m * ↑(n.choose m) = 0
Nat.sum_range_add_choose 📋 Mathlib.Data.Nat.Choose.Sum
(n k : ℕ) : ∑ i ∈ Finset.range (n + 1), (i + k).choose k = (n + k + 1).choose (k + 1)
Nat.sum_range_mul_choose 📋 Mathlib.Data.Nat.Choose.Sum
(n : ℕ) : ∑ i ∈ Finset.range (n + 1), i * n.choose i = n * 2 ^ (n - 1)
Int.alternating_sum_range_choose 📋 Mathlib.Data.Nat.Choose.Sum
{n : ℕ} : ∑ m ∈ Finset.range (n + 1), (-1) ^ m * ↑(n.choose m) = if n = 0 then 1 else 0
Int.alternating_sum_range_choose_eq_choose 📋 Mathlib.Data.Nat.Choose.Sum
{n m : ℕ} : ∑ k ∈ Finset.range (m + 1), (-1) ^ k * ↑((n + 1).choose k) = (-1) ^ m * ↑(n.choose m)
Commute.add_pow 📋 Mathlib.Data.Nat.Choose.Sum
{R : Type u_1} [Semiring R] {x y : R} (h : Commute x y) (n : ℕ) : (x + y) ^ n = ∑ m ∈ Finset.range (n + 1), x ^ m * y ^ (n - m) * ↑(n.choose m)
add_pow 📋 Mathlib.Data.Nat.Choose.Sum
{R : Type u_1} [CommSemiring R] (x y : R) (n : ℕ) : (x + y) ^ n = ∑ m ∈ Finset.range (n + 1), x ^ m * y ^ (n - m) * ↑(n.choose m)
Finset.prod_pow_choose_succ 📋 Mathlib.Data.Nat.Choose.Sum
{M : Type u_2} [CommMonoid M] (f : ℕ → ℕ → M) (n : ℕ) : ∏ i ∈ Finset.range (n + 2), f i (n + 1 - i) ^ (n + 1).choose i = (∏ i ∈ Finset.range (n + 1), f i (n + 1 - i) ^ n.choose i) * ∏ i ∈ Finset.range (n + 1), f (i + 1) (n - i) ^ n.choose i
Finset.sum_choose_succ_nsmul 📋 Mathlib.Data.Nat.Choose.Sum
{M : Type u_2} [AddCommMonoid M] (f : ℕ → ℕ → M) (n : ℕ) : ∑ i ∈ Finset.range (n + 2), (n + 1).choose i • f i (n + 1 - i) = ∑ i ∈ Finset.range (n + 1), n.choose i • f i (n + 1 - i) + ∑ i ∈ Finset.range (n + 1), n.choose i • f (i + 1) (n - i)
sub_pow 📋 Mathlib.Data.Nat.Choose.Sum
{R : Type u_1} [CommRing R] (x y : R) (n : ℕ) : (x - y) ^ n = ∑ m ∈ Finset.range (n + 1), (-1) ^ (m + n) * x ^ m * y ^ (n - m) * ↑(n.choose m)
Finset.sum_choose_succ_mul 📋 Mathlib.Data.Nat.Choose.Sum
{R : Type u_1} [NonAssocSemiring R] (f : ℕ → ℕ → R) (n : ℕ) : ∑ i ∈ Finset.range (n + 2), ↑((n + 1).choose i) * f i (n + 1 - i) = ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * f i (n + 1 - i) + ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * f (i + 1) (n - i)
Finset.sort_range 📋 Mathlib.Data.Finset.Sort
(n : ℕ) : ((Finset.range n).sort fun a b => a ≤ b) = List.range n
Polynomial.eval_geom_sum 📋 Mathlib.Algebra.Polynomial.Eval.Defs
{R : Type u_1} [CommSemiring R] {n : ℕ} {x : R} : Polynomial.eval x (∑ i ∈ Finset.range n, Polynomial.X ^ i) = ∑ i ∈ Finset.range n, x ^ i
Polynomial.one_add_X_pow_sub_X_pow 📋 Mathlib.Algebra.Polynomial.Coeff
{S : Type u_1} [CommRing S] (d : ℕ) : (1 + Polynomial.X) ^ d - Polynomial.X ^ d = ∑ i ∈ Finset.range d, d.choose i • Polynomial.X ^ i
Polynomial.supp_subset_range 📋 Mathlib.Algebra.Polynomial.Degree.Support
{R : Type u} {m : ℕ} [Semiring R] {p : Polynomial R} (h : p.natDegree < m) : p.support ⊆ Finset.range m
Polynomial.supp_subset_range_natDegree_succ 📋 Mathlib.Algebra.Polynomial.Degree.Support
{R : Type u} [Semiring R] {p : Polynomial R} : p.support ⊆ Finset.range (p.natDegree + 1)
Polynomial.sum_over_range' 📋 Mathlib.Algebra.Polynomial.Degree.Support
{R : Type u} {S : Type v} [Semiring R] [AddCommMonoid S] (p : Polynomial R) {f : ℕ → R → S} (h : ∀ (n : ℕ), f n 0 = 0) (n : ℕ) (hn : p.natDegree < n) : p.sum f = ∑ a ∈ Finset.range n, f a (p.coeff a)
Polynomial.sum_over_range 📋 Mathlib.Algebra.Polynomial.Degree.Support
{R : Type u} {S : Type v} [Semiring R] [AddCommMonoid S] (p : Polynomial R) {f : ℕ → R → S} (h : ∀ (n : ℕ), f n 0 = 0) : p.sum f = ∑ a ∈ Finset.range (p.natDegree + 1), f a (p.coeff a)
Polynomial.as_sum_range' 📋 Mathlib.Algebra.Polynomial.Degree.Support
{R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (hn : p.natDegree < n) : p = ∑ i ∈ Finset.range n, (Polynomial.monomial i) (p.coeff i)
Polynomial.as_sum_range 📋 Mathlib.Algebra.Polynomial.Degree.Support
{R : Type u} [Semiring R] (p : Polynomial R) : p = ∑ i ∈ Finset.range (p.natDegree + 1), (Polynomial.monomial i) (p.coeff i)
Polynomial.as_sum_range_C_mul_X_pow' 📋 Mathlib.Algebra.Polynomial.Degree.Support
{R : Type u} [Semiring R] (p : Polynomial R) {n : ℕ} (hn : p.natDegree < n) : p = ∑ i ∈ Finset.range n, Polynomial.C (p.coeff i) * Polynomial.X ^ i
Polynomial.as_sum_range_C_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Degree.Support
{R : Type u} [Semiring R] (p : Polynomial R) : p = ∑ i ∈ Finset.range (p.natDegree + 1), Polynomial.C (p.coeff i) * Polynomial.X ^ i
Polynomial.eval_eq_sum_range' 📋 Mathlib.Algebra.Polynomial.Eval.Degree
{R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (hn : p.natDegree < n) (x : R) : Polynomial.eval x p = ∑ i ∈ Finset.range n, p.coeff i * x ^ i
Polynomial.eval_eq_sum_range 📋 Mathlib.Algebra.Polynomial.Eval.Degree
{R : Type u} [Semiring R] {p : Polynomial R} (x : R) : Polynomial.eval x p = ∑ i ∈ Finset.range (p.natDegree + 1), p.coeff i * x ^ i
Polynomial.eval₂_eq_sum_range' 📋 Mathlib.Algebra.Polynomial.Eval.Degree
{R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) {p : Polynomial R} {n : ℕ} (hn : p.natDegree < n) (x : S) : Polynomial.eval₂ f x p = ∑ i ∈ Finset.range n, f (p.coeff i) * x ^ i
Polynomial.eval₂_eq_sum_range 📋 Mathlib.Algebra.Polynomial.Eval.Degree
{R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (x : S) : Polynomial.eval₂ f x p = ∑ i ∈ Finset.range (p.natDegree + 1), f (p.coeff i) * x ^ i
Polynomial.eval_monomial_one_add_sub 📋 Mathlib.Algebra.Polynomial.Eval.Degree
{S : Type v} [CommRing S] (d : ℕ) (y : S) : Polynomial.eval (1 + y) ((Polynomial.monomial d) (↑d + 1)) - Polynomial.eval y ((Polynomial.monomial d) (↑d + 1)) = ∑ x_1 ∈ Finset.range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))
Polynomial.aeval_eq_sum_range' 📋 Mathlib.Algebra.Polynomial.AlgebraMap
{R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {p : Polynomial R} {n : ℕ} (hn : p.natDegree < n) (x : S) : (Polynomial.aeval x) p = ∑ i ∈ Finset.range n, p.coeff i • x ^ i
Polynomial.aeval_eq_sum_range 📋 Mathlib.Algebra.Polynomial.AlgebraMap
{R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {p : Polynomial R} (x : S) : (Polynomial.aeval x) p = ∑ i ∈ Finset.range (p.natDegree + 1), p.coeff i • x ^ i
Polynomial.Monic.as_sum 📋 Mathlib.Algebra.Polynomial.Monic
{R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) : p = Polynomial.X ^ p.natDegree + ∑ i ∈ Finset.range p.natDegree, Polynomial.C (p.coeff i) * Polynomial.X ^ i
geom_sum_zero 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [Semiring R] (x : R) : ∑ i ∈ Finset.range 0, x ^ i = 0
geom_sum_one 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [Semiring R] (x : R) : ∑ i ∈ Finset.range 1, x ^ i = 1
one_geom_sum 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [Semiring R] (n : ℕ) : ∑ i ∈ Finset.range n, 1 ^ i = ↑n
geom_sum_two 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [Semiring R] {x : R} : ∑ i ∈ Finset.range 2, x ^ i = x + 1
op_geom_sum 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [Semiring R] (x : R) (n : ℕ) : MulOpposite.op (∑ i ∈ Finset.range n, x ^ i) = ∑ i ∈ Finset.range n, MulOpposite.op x ^ i
Nat.geomSum_eq 📋 Mathlib.Algebra.Ring.GeomSum
{m : ℕ} (hm : 2 ≤ m) (n : ℕ) : ∑ k ∈ Finset.range n, m ^ k = (m ^ n - 1) / (m - 1)
zero_geom_sum 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [Semiring R] {n : ℕ} : ∑ i ∈ Finset.range n, 0 ^ i = if n = 0 then 0 else 1
neg_one_geom_sum 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [Ring R] {n : ℕ} : ∑ i ∈ Finset.range n, (-1) ^ i = if Even n then 0 else 1
geom_sum_succ' 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [Semiring R] {x : R} {n : ℕ} : ∑ i ∈ Finset.range (n + 1), x ^ i = x ^ n + ∑ i ∈ Finset.range n, x ^ i
geom_sum_succ 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [Semiring R] {x : R} {n : ℕ} : ∑ i ∈ Finset.range (n + 1), x ^ i = x * ∑ i ∈ Finset.range n, x ^ i + 1
RingHom.map_geom_sum 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (x : R) (n : ℕ) (f : R →+* S) : f (∑ i ∈ Finset.range n, x ^ i) = ∑ i ∈ Finset.range n, f x ^ i
geom_sum₂_with_one 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [Semiring R] (x : R) (n : ℕ) : ∑ i ∈ Finset.range n, x ^ i * 1 ^ (n - 1 - i) = ∑ i ∈ Finset.range n, x ^ i
geom_sum_mul 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [Ring R] (x : R) (n : ℕ) : (∑ i ∈ Finset.range n, x ^ i) * (x - 1) = x ^ n - 1
geom_sum_mul_neg 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [Ring R] (x : R) (n : ℕ) : (∑ i ∈ Finset.range n, x ^ i) * (1 - x) = 1 - x ^ n
mul_geom_sum 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [Ring R] (x : R) (n : ℕ) : (x - 1) * ∑ i ∈ Finset.range n, x ^ i = x ^ n - 1
mul_neg_geom_sum 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [Ring R] (x : R) (n : ℕ) : (1 - x) * ∑ i ∈ Finset.range n, x ^ i = 1 - x ^ n
geom_sum₂_self 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [Semiring R] (x : R) (n : ℕ) : ∑ i ∈ Finset.range n, x ^ i * x ^ (n - 1 - i) = ↑n * x ^ (n - 1)
geom_sum_mul_add 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [Semiring R] (x : R) (n : ℕ) : (∑ i ∈ Finset.range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n
Commute.geom_sum₂_comm 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [Semiring R] {x y : R} (n : ℕ) (h : Commute x y) : ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = ∑ i ∈ Finset.range n, y ^ i * x ^ (n - 1 - i)
geom_sum₂_comm 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [CommSemiring R] (x y : R) (n : ℕ) : ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = ∑ i ∈ Finset.range n, y ^ i * x ^ (n - 1 - i)
Commute.geom_sum₂_mul_add 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [Semiring R] {x y : R} (h : Commute x y) (n : ℕ) : (∑ i ∈ Finset.range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n
geom_sum₂_mul_add 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [CommSemiring R] (x y : R) (n : ℕ) : (∑ i ∈ Finset.range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n
Commute.geom_sum₂_mul 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [Ring R] {x y : R} (h : Commute x y) (n : ℕ) : (∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
Commute.mul_geom_sum₂ 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [Ring R] {x y : R} (h : Commute x y) (n : ℕ) : (x - y) * ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = x ^ n - y ^ n
Commute.mul_neg_geom_sum₂ 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [Ring R] {x y : R} (h : Commute x y) (n : ℕ) : (y - x) * ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = y ^ n - x ^ n
geom_sum₂_mul 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [CommRing R] (x y : R) (n : ℕ) : (∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
geom_sum_mul_of_le_one 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [CommSemiring R] [PartialOrder R] [AddLeftReflectLE R] [AddLeftMono R] [ExistsAddOfLE R] [Sub R] [OrderedSub R] {x : R} (hx : x ≤ 1) (n : ℕ) : (∑ i ∈ Finset.range n, x ^ i) * (1 - x) = 1 - x ^ n
geom_sum_mul_of_one_le 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [CommSemiring R] [PartialOrder R] [AddLeftReflectLE R] [AddLeftMono R] [ExistsAddOfLE R] [Sub R] [OrderedSub R] {x : R} (hx : 1 ≤ x) (n : ℕ) : (∑ i ∈ Finset.range n, x ^ i) * (x - 1) = x ^ n - 1
pow_sub_one_mul_geom_sum_eq_pow_sub_one_mul_geom_sum 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [CommRing R] {x : R} {m n : ℕ} : (x ^ m - 1) * ∑ k ∈ Finset.range n, x ^ k = (x ^ n - 1) * ∑ k ∈ Finset.range m, x ^ k
op_geom_sum₂ 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [Semiring R] (x y : R) (n : ℕ) : ∑ i ∈ Finset.range n, MulOpposite.op y ^ (n - 1 - i) * MulOpposite.op x ^ i = ∑ i ∈ Finset.range n, MulOpposite.op y ^ i * MulOpposite.op x ^ (n - 1 - i)
geom_sum₂_mul_of_ge 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [CommSemiring R] [PartialOrder R] [AddLeftReflectLE R] [AddLeftMono R] [ExistsAddOfLE R] [Sub R] [OrderedSub R] {x y : R} (hxy : y ≤ x) (n : ℕ) : (∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
geom_sum₂_mul_of_le 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [CommSemiring R] [PartialOrder R] [AddLeftReflectLE R] [AddLeftMono R] [ExistsAddOfLE R] [Sub R] [OrderedSub R] {x y : R} (hxy : x ≤ y) (n : ℕ) : (∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)) * (y - x) = y ^ n - x ^ n
Commute.geom_sum₂_succ_eq 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [Ring R] {x y : R} (h : Commute x y) {n : ℕ} : ∑ i ∈ Finset.range (n + 1), x ^ i * y ^ (n - i) = x ^ n + y * ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)
RingHom.map_geom_sum₂ 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (x y : R) (n : ℕ) (f : R →+* S) : f (∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)) = ∑ i ∈ Finset.range n, f x ^ i * f y ^ (n - 1 - i)
geom_sum₂_succ_eq 📋 Mathlib.Algebra.Ring.GeomSum
{R : Type u_1} [CommRing R] (x y : R) {n : ℕ} : ∑ i ∈ Finset.range (n + 1), x ^ i * y ^ (n - i) = x ^ n + y * ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)
Polynomial.monic_geom_sum_X 📋 Mathlib.RingTheory.Polynomial.Basic
{R : Type u} [Semiring R] {n : ℕ} (hn : n ≠ 0) : (∑ i ∈ Finset.range n, Polynomial.X ^ i).Monic
Polynomial.Monic.geom_sum 📋 Mathlib.RingTheory.Polynomial.Basic
{R : Type u} [Semiring R] {P : Polynomial R} (hP : P.Monic) (hdeg : 0 < P.natDegree) {n : ℕ} (hn : n ≠ 0) : (∑ i ∈ Finset.range n, P ^ i).Monic
Polynomial.Monic.geom_sum' 📋 Mathlib.RingTheory.Polynomial.Basic
{R : Type u} [Semiring R] {P : Polynomial R} (hP : P.Monic) (hdeg : 0 < P.degree) {n : ℕ} (hn : n ≠ 0) : (∑ i ∈ Finset.range n, P ^ i).Monic

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. 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:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
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
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.
You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

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. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c