Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-12 09:31 0f6b3ca4

View on Github →

doc(data/complex/basic): docstrings and pp_nodots (#3044)

Estimated changes

modified def complex.norm_sq