Mathlib v3 is deprecated. Go to Mathlib v4

Def complex.lift_aux

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