Theorem selfAdjoint.imaginaryPart_coe

Modification history

2025-10-08 02:50
Mathlib/LinearAlgebra/Complex/Module.lean
feat: add lemmata about selfadjoint elements (#30301) …
Added selfAdjoint.imaginaryPart_coeView on Github →