Zulip Chat Archive

Stream: mathlib4

Topic: pow_succ

Ruben Van de Velde (Dec 22 2022 at 13:53):

It seems like pow_succ changed from a ^ (n + 1) = a * a ^ n in mathlib3 to n^(succ m) = n^m * n in lean4 core :/

Yaël Dillies (Dec 22 2022 at 13:54):

docs4#pow_succ

Yaël Dillies (Dec 22 2022 at 13:54):

You mean docs4#Nat.pow_succ?

Ruben Van de Velde (Dec 22 2022 at 13:55):

Yeah, apparently I was picking that up

Ruben Van de Velde (Dec 22 2022 at 13:55):

Is that better or worse?

Yaël Dillies (Dec 22 2022 at 13:56):

It should be protected but apart from that I don't think that's a problem. What docs#nat.pow_succ?

Yaël Dillies (Dec 22 2022 at 13:56):

Ahah, it's not a thing.

Ruben Van de Velde (Dec 22 2022 at 14:02):

Oh no, it seems like my issue was that I was picking up Nat.pow_succ' (https://leanprover-community.github.io/mathlib4_docs/Std/Data/Nat/Lemmas.html#Nat.pow_succ') - from Std - rather than pow_succ' (https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Group/Commute.html#pow_succ') (and the primes seem to confuse the docs search)

Edit: they also confuse Zulip

Last updated: Dec 20 2023 at 11:08 UTC