mathlib3
7ab3af8f - chore(data.nat.prime): reduce imports (#17840)
Commit
View On GitHub
Commit
3 years ago
chore(data.nat.prime): reduce imports (#17840)
Parents
48c518de
FAQ Terms Privacy Refunds Impressum
Loading