Theorem IsSelfAdjoint.I_smul_of_mem_skewAdjoint

Modification history

2026-06-16 23:11
Mathlib/Analysis/RCLike/Basic.lean
feat: some API for relating self-adjoint and skew-adjoints (#40684)
Added IsSelfAdjoint.I_smul_of_mem_skewAdjointView on Github →