Theorem selfAdjoint.realPart_coe

Modification history

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