mathlib3
29beb1f3 - feat(analysis/normed_space/int): norms of (units of) integers (#8136)

Commit

4 years ago

feat(analysis/normed_space/int): norms of (units of) integers (#8136) From LTE

Author

jcommelin

jcommelin

Parents

Loading