Commit 2025-08-26 17:10 0e9d0eca

View on Github →

feat(Analysis/InnerProductSpace/IsPositive): (adjoint S ∘ S).IsPositive and (S ∘ adjoint S).IsPositive (#28338)

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Positive.lean

added theorem ContinuousLinearMap.isPositive_adjoint_comp_self

added theorem ContinuousLinearMap.isPositive_self_comp_adjoint

added theorem LinearMap.isPositive_adjoint_comp_self

added theorem LinearMap.isPositive_self_comp_adjoint