Theorem complex.continuous_conj
Modification history
2022-05-04 07:50
src/analysis/complex/basic.lean
feat(topology/algebra/star): continuity of `star` (#13855) …
Modified complex.continuous_conjView on Github →2021-10-21 23:04
src/analysis/complex/basic.lean
refactor(data/complex/*): replace `complex.conj` and `is_R_or_C.conj` with star (#9640) …
Modified complex.continuous_conjView on Github →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) …
Modified complex.continuous_conjView on Github →