Zulip Chat Archive

Stream: maths

Topic: making PR about transcendental numbers


view this post on Zulip Jujian Zhang (Aug 19 2020 at 22:28):

Hello everyone, I am trying to make a new PR about transcendental numbers. Which subdirectories should I put everything in? Should it be under src/analysis?

view this post on Zulip Mario Carneiro (Aug 19 2020 at 22:30):

analysis.transcendental sounds good to me

view this post on Zulip Jujian Zhang (Aug 20 2020 at 17:27):

Can I have permission to push to mathlib please

view this post on Zulip Jujian Zhang (Aug 20 2020 at 17:28):

GitHub user name is jjaassoonn

view this post on Zulip Bryan Gin-ge Chen (Aug 20 2020 at 17:30):

@Jujian Zhang Invite sent! https://github.com/leanprover-community/mathlib/invitations

view this post on Zulip Jujian Zhang (Aug 20 2020 at 17:31):

Thank you

view this post on Zulip Jujian Zhang (Aug 20 2020 at 17:32):

Sorry for the stupid question, but how does this link work? When I click it, it says 404

view this post on Zulip Jujian Zhang (Aug 20 2020 at 17:33):

@Bryan Gin-ge Chen

view this post on Zulip Bryan Gin-ge Chen (Aug 20 2020 at 17:33):

I believe you have to be logged into Github for it to work.

view this post on Zulip Jujian Zhang (Aug 20 2020 at 17:34):

Oh right! Sorry


Last updated: May 09 2021 at 10:11 UTC