Theorem IsSelfAdjoint.imaginaryPart

Modification history

2023-10-31 09:38

Mathlib/Data/Complex/Module.lean

chore: bump toolchain to v4.3.0-rc1 (#8051) …

Deleted IsSelfAdjoint.imaginaryPart View on Github →

2023-09-08 11:01

Mathlib/Data/Complex/Module.lean

feat: flesh out the API for `realPart` and `imaginaryPart` (#7023) …

Added IsSelfAdjoint.imaginaryPart View on Github →