Zulip Chat Archive
Stream: new members
Topic: Import Mathlib not working as Expected
Guest User (Oct 17 2024 at 23:59):
Could anyone please help me resolve this issue?
Guest User (Oct 18 2024 at 00:03):
Notification Bot (Oct 18 2024 at 00:05):
2 messages were moved here from #general > Import Mathlib not working as Expected by Eric Wieser.
Eric Wieser (Oct 18 2024 at 00:06):
Your thread title is misleading; does import Mathlib (not import Mathlib.Algebra....) work as expected?
Guest User (Oct 18 2024 at 00:10):
Eric Wieser said:
Your thread title is misleading; does
import Mathlib(notimport Mathlib.Algebra....) work as expected?
No
Kevin Buzzard (Oct 18 2024 at 07:38):
Did you try what it suggests at the top of the error message?
Last updated: May 02 2025 at 03:31 UTC