Theorem Complex.I_smul_mem_skewAdjoint_iff_isSelfAdjoint

Modification history

2026-06-16 23:11
Mathlib/LinearAlgebra/Complex/Module.lean
feat: some API for relating self-adjoint and skew-adjoints (#40684)
Added Complex.I_smul_mem_skewAdjoint_iff_isSelfAdjointView on Github →