Theorem imaginaryPart_eq_neg_I_smul_skewAdjointPart

Modification history

2023-09-08 11:01
Mathlib/Data/Complex/Module.lean
feat: flesh out the API for `realPart` and `imaginaryPart` (#7023) …
Added imaginaryPart_eq_neg_I_smul_skewAdjointPartView on Github →