mathlib3
3a5851f0 - feat(data/complex/module): add complex.lift to match zsqrtd.lift (#8107)

Commit
4 years ago
feat(data/complex/module): add complex.lift to match zsqrtd.lift (#8107) [Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/The.20unique.20.60.E2.84.82.20.E2.86.92.E2.82.90.5B.E2.84.9D.5D.20A.60.20given.20a.20square.20root.20of.20-1/near/244135262)
Author
Parents
Loading