Mathlib v3 is deprecated. Go to Mathlib v4

Theorem complex.eq_re_of_real_le

Modification history

2022-10-27 03:22

src/data/complex/basic.lean

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

Added complex.eq_re_of_real_le View on Github →