Zulip Chat Archive

Stream: general

Topic: abel idempotence


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 01 2020 at 19:41):

#mwe

view this post on Zulip Reid Barton (May 01 2020 at 20:24):

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

view this post on Zulip 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.

view this post on Zulip 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