mathlib3
6a449305 - refactor(data/pnat): move data.pnat.prime (#4839)

Commit

5 years ago

refactor(data/pnat): move data.pnat.prime (#4839) Remove the dependency `data.pnat.basic -> data.nat.prime`. Needed for #4822.

References

Author

digama0

Parents