Theorem Complex.coe_realPart

Modification history

2026-06-16 23:11

Mathlib/LinearAlgebra/Complex/Module.lean

feat: some API for relating self-adjoint and skew-adjoints (#40684)

Modified Complex.coe_realPart View on Github →

2023-09-08 11:01

Mathlib/Data/Complex/Module.lean

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

Added Complex.coe_realPart View on Github →