Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-30 18:03 3a5851f0

View on Github →

feat(data/complex/module): add complex.lift to match zsqrtd.lift (#8107) Zulip

Estimated changes

Modified src/data/complex/module.lean

added def complex.lift_aux

added theorem complex.lift_aux_I

added theorem complex.lift_aux_apply

added theorem complex.lift_aux_apply_I

added theorem complex.lift_aux_neg_I