Commit 2026-06-16 23:11 9c1fa80c

View on Github →

feat: some API for relating self-adjoint and skew-adjoints (#40684)

Estimated changes

Modified Mathlib/Analysis/RCLike/Basic.lean

added theorem IsSelfAdjoint.I_smul_mem_skewAdjoint

added theorem IsSelfAdjoint.I_smul_of_mem_skewAdjoint

added theorem RCLike.I_mem_skewAdjoint

Modified Mathlib/LinearAlgebra/Complex/Module.lean

added theorem Complex.I_mem_skewAdjoint

added theorem Complex.I_smul_mem_skewAdjoint_iff_isSelfAdjoint

modified theorem Complex.coe_realPart

added theorem Complex.isSelfAdjoint_I_smul_iff_mem_skewAdjoint