no goals
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f : α → β
inst✝ : CommMonoid β
n : ℕ
⊢ (∑ i in range n, i) * 2 = ∑ i in range n, i + ∑ i in range n, (n - 1 - i)
rw [sum_range_reflect (fun i => i) n, mul_two]
no goals
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f : α → β
inst✝ : CommMonoid β
n : ℕ
⊢ ∑ i in range n, (n - 1) = n * (n - 1)
rw [sum_const, card_range, Nat.nsmul_eq_mul]