mathlib3
9f6300e9 - chore(data/complex/basic): upgrade `complex.norm_sq` to a `monoid_with_zero_hom` (#5553)

Commit
4 years ago
chore(data/complex/basic): upgrade `complex.norm_sq` to a `monoid_with_zero_hom` (#5553)
Author
Parents
Loading