Commit 2025-07-13 04:28 0704f766
View on Github →feat(Analysis/InnerProductSpace/Adjoint): idempotent operator T
is self-adjoint iff (range T)ᗮ = ker T
(#26855)
This adds that an idempotent operator T
is self-adjoint iff (range T)ᗮ = ker T
.
feat(Analysis/InnerProductSpace/Adjoint): idempotent operator T
is self-adjoint iff (range T)ᗮ = ker T
(#26855)
This adds that an idempotent operator T
is self-adjoint iff (range T)ᗮ = ker T
.