Mathlib v3 is deprecated. Go to Mathlib v4

Theorem complex.conj_cle_coe

Modification history

2021-06-25 10:35

src/analysis/complex/basic.lean

chore(data/complex/{module, is_R_or_C}, analysis/complex/basic): rationalize the structure provided for `conj` and `of_real` (#8014) …

Added complex.conj_cle_coe View on Github →