mathlib
23e0e290 - chore(*): register global fact instances (#11749)

Commit
3 years ago
chore(*): register global fact instances (#11749) We register globally some fact instances which are necessary for integration or euclidean spaces. And also the fact that 2 and 3 are prime. See https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/euclidean_space.20error/near/269992165
Author
Parents
Loading