Commit 2022-02-01 12:46 23e0e290
View on Github →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