Theorem map_realPart

Modification history

2026-06-23 15:06
Mathlib/LinearAlgebra/Complex/Module.lean
feat: introduce `SelfAdjointDecompose` class (#40530)
Added map_realPartView on Github →