Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-04 15:24 6e94c53a

View on Github →

feat(complex/basic): nnnorm coercions (#12428)

Estimated changes

Modified src/analysis/complex/basic.lean

added theorem complex.nnnorm_eq_one_of_pow_eq_one

added theorem complex.nnnorm_int

added theorem complex.nnnorm_nat

added theorem complex.nnnorm_real

added theorem complex.norm_eq_one_of_pow_eq_one

Modified src/analysis/complex/roots_of_unity.lean

added theorem is_primitive_root.nnnorm_eq_one