Def complex.lift

Modification history

2021-07-07 17:46
src/data/complex/module.lean
fix(data/complex/basic): ensure `algebra ℝ ℂ` is computable (#8166) …
Added complex.liftView on Github →