Mathlib v3 is deprecated. Go to Mathlib v4

Theorem complex.coe_re

Modification history

2018-01-20 17:03

data/complex.lean

refactor(data/complex): clean up proofs

Deleted complex.coe_re View on Github →

2018-01-07 14:32

analysis/complex.lean

feat(analysis/complex): complex numbers as a field

Added complex.coe_re View on Github →