mathlib3
c782e282 - chore(analysis/normed_space/units): add `protected`, minor review (#6544)

Commit

4 years ago

chore(analysis/normed_space/units): add `protected`, minor review (#6544)

Author

urkud

urkud

Parents

Loading