Mathlib v3 is deprecated. Go to Mathlib v4

Theorem complex.norm_sq_apply

Modification history

2021-01-02 10:18

src/data/complex/basic.lean

chore(data/complex/basic): upgrade `complex.norm_sq` to a `monoid_with_zero_hom` (#5553)

Added complex.norm_sq_apply View on Github →