mathlib3
c8fd7e33
- chore(measure_theory/covering/besicovitch): Weaker import (#11763)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
chore(measure_theory/covering/besicovitch): Weaker import (#11763) We relax the `set_theory.cardinal_ordinal` import to the weaker `set_theory.ordinal_arithmetic` import. We also fix some trivial spacing issues in the docs.
Author
vihdzp
Parents
a18680a6
Loading