Mathlib v3 is deprecated. Go to Mathlib v4

Theorem complex.cos_sq_add_sin_sq

Modification history

2020-12-10 21:44

src/data/complex/exponential.lean

chore(data/complex/exponential): add `inv_one_add_tan_sq` etc (#5299) …

Added complex.cos_sq_add_sin_sq View on Github →