Mathlib v3 is deprecated. Go to Mathlib v4

Theorem complex.conj_ae_coe

Modification history

2021-06-25 10:35

src/data/complex/module.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_ae_coe View on Github →