Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-26 18:22 bd21b0ed

View on Github →

feat(analyis/normed_space): add normed_field instance for ℂ

Estimated changes

added theorem complex.norm_int
added theorem complex.norm_nat
added theorem complex.norm_rat
added theorem complex.norm_real