Mathlib v3 is deprecated. Go to Mathlib v4

Def complex.norm_squared

Modification history

2018-01-20 17:03

data/complex.lean

refactor(data/complex): clean up proofs

Deleted complex.norm_squared View on Github →

2018-01-07 14:32

analysis/complex.lean

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

Added complex.norm_squared View on Github →