Zulip Chat Archive

Stream: new members

Topic: importing mathlib4

Daniel Donnelly (May 21 2023 at 22:09):

@Kevin Buzzard What are the instructions again to import Mathlib4 successfully? I can't find that Zulip thread anywhere! :)

Scott Morrison (May 22 2023 at 02:05):

@Daniel Donnelly, I'm moving this to the new members stream. Perhaps you can explain in more detail what you mean? Importing all of mathlib is just import Mathlib.

Notification Bot (May 22 2023 at 02:05):

2 messages were moved here from #mathlib4 > !4#4047 Analysis.Normed.Group.SemiNormedGroup by Scott Morrison.

Kevin Buzzard (May 22 2023 at 04:22):

If this is about creating projects, then the answers should be on the Mathlib4 README.

Last updated: Dec 20 2023 at 11:08 UTC