Mathlib Changelog
v4
Changelog
About
Github
Theorem
RCLike.I_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
RCLike.I_mem_skewAdjoint
View on Github →