Commit 2025-09-12 23:06 bf8a2e55

View on Github →

feat(Analysis/InnerProductSpace/LinearPMap): the adjoint is closed (#29595) Define the graph of the adjoint and prove that the adjoint operator is always closed. Author: Moritz Doll moritz.doll@googlemail.com

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/LinearPMap.lean

added theorem IsSelfAdjoint.isClosed

added theorem LinearPMap.adjoint_graph_eq_graph_adjoint

added theorem LinearPMap.adjoint_isClosed

added theorem LinearPMap.graph_adjoint_toLinearPMap_eq_adjoint

added def Submodule.adjoint

added theorem Submodule.mem_adjoint_iff

Modified Mathlib/LinearAlgebra/Prod.lean

added theorem LinearEquiv.skewSwap_apply

added theorem LinearEquiv.skewSwap_symm_apply