Theorem map_imaginaryPart

Modification history

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