Zulip Chat Archive

Stream: mathlib4

Topic: add_pow

Andrew Wheen (Dec 09 2022 at 08:21):

Has add_pow (binomial theorem) been ported to mathlib4 yet? I can only find it for Lean3.

Kevin Buzzard (Dec 09 2022 at 08:36):

Check the top of the file where it's defined in lean 3 and see if there's a message saying "this file has been ported to lean 4" or not.

Alex J. Best (Dec 09 2022 at 08:38):

https://leanprover-community.github.io/mathlib4_docs/ implies the answer is no, and it is fairly up to date now. I don't even think mathlib4 has the definition of choose or factorial yet so this is probably a few weeks away.

Patrick Massot (Dec 09 2022 at 08:44):

See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/port.20progress/near/314816205

Andrew Wheen (Dec 09 2022 at 08:47):

Many thanks for the replies. I'll keep an eye out for it.

Last updated: Dec 20 2023 at 11:08 UTC