Mathlib v3 is deprecated. Go to Mathlib v4

Def complex.of_real_am

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