Theorem Complex.isSelfAdjoint_I_smul_iff_mem_skewAdjoint

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.isSelfAdjoint_I_smul_iff_mem_skewAdjointView on Github →