Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-27 03:22 05f9a362

View on Github →

feat({data, analysis}/complex/basic): lemmas related to complex.partial_order (#17170)

Estimated changes

Modified src/analysis/complex/basic.lean

added theorem complex.eq_coe_norm_of_nonneg

Modified src/data/complex/basic.lean

added theorem complex.eq_re_of_real_le