Commit 2022-10-10 08:47 103252ae
View on Github →chore(data/int/gcd): streamline imports (#16811)
The file on gcds of integers is fundamentally very elementary, but it contained two lemmas about prime numbers, and data.nat.prime seems to import everything (modules! half the order library!).