Mathlib v3 is deprecated. Go to Mathlib v4

Theorem complex.lift_aux_apply_I

Modification history

2021-06-30 18:03
src/data/complex/module.lean
feat(data/complex/module): add complex.lift to match zsqrtd.lift (#8107) …
Added complex.lift_aux_apply_IView on Github →