mathlib3
ba80091d - feat(data/complex/basic): bundle complex.abs (#16347)

Commit
3 years ago
feat(data/complex/basic): bundle complex.abs (#16347) Doing this this way round makes the refactor in #16340 much easier. I will follow up this PR with similar PRs for `padic_norm` and `padic_norm_e`. Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>
Author
Parents
Loading