Commit 2023-10-16 02:18 7f121a48

View on Github →

feat(Analysis/InnerProductSpace/LinearPMap): the adjoint is closed (#6537) Define the graph of the adjoint and prove that the adjoint operator is always closed.

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