## Stream: general

### Topic: abel idempotence

#### Johan Commelin (May 01 2020 at 19:33):

Should abel be idempotent?

import analysis.specific_limits

example {α : Type u_1} [normed_group α] {r C : ℝ} (n : ℕ)
{f : ℕ → α} (hf : ∀ (n : ℕ), ∥f n∥ ≤ C * r ^ n) :
-((∑ (i : ℕ) in range n, f i) - (f n + ∑ (x : ℕ) in range n, f x)) = f n :=
begin
abel, -- does not close the goal
abel, -- closes the goal
end


#### Kevin Buzzard (May 01 2020 at 19:40):

I saw this once with ring and what was happening was that there was some metavariable goal

#mwe

#### Reid Barton (May 01 2020 at 20:24):

I just deleted {ring, ring} from my project today!

#### Rob Lewis (May 01 2020 at 21:59):

@Bryan Gin-ge Chen I hope the banana means that I'm not the only one with Raffi stuck in my head now.

#### Bryan Gin-ge Chen (May 01 2020 at 22:27):

Yes! Though I've never much minded having songs stuck in my head.

Slightly more on topic, is there a way to cook up examples which require {ring, ring, ring} (or even more)?

Last updated: May 08 2021 at 09:11 UTC