Def complex.conj_lie

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_lie View on Github →