mathlib3
249a015c
- chore(ring_theory/coprime): split out imports into a new file so that `is_coprime` can be used earlier. (#9403)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
4 years ago
chore(ring_theory/coprime): split out imports into a new file so that `is_coprime` can be used earlier. (#9403) [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Use.20of.20is_coprime.20in.20rat.2Ebasic/near/254942750)
Author
eric-wieser
Parents
102ce303
Loading