Commit 2023-06-27 14:11 96296467

View on Github →

feat: port Analysis.InnerProductSpace.LinearPMap (#5523)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/InnerProductSpace/LinearPMap.lean

added theorem ContinuousLinearMap.toPMap_adjoint_eq_adjoint_toPMap_of_dense

added theorem LinearPMap.IsFormalAdjoint.le_adjoint

added def LinearPMap.IsFormalAdjoint

added def LinearPMap.adjoint

added def LinearPMap.adjointAux

added theorem LinearPMap.adjointAux_inner

added theorem LinearPMap.adjointAux_unique

added def LinearPMap.adjointDomain

added def LinearPMap.adjointDomainMkClm

added def LinearPMap.adjointDomainMkClmExtend

added theorem LinearPMap.adjointDomainMkClmExtend_apply

added theorem LinearPMap.adjointDomainMkClm_apply

added theorem LinearPMap.adjoint_apply_eq

added theorem LinearPMap.adjoint_apply_of_dense

added theorem LinearPMap.adjoint_apply_of_not_dense

added theorem LinearPMap.adjoint_isFormalAdjoint

added theorem LinearPMap.mem_adjoint_domain_iff

added theorem LinearPMap.mem_adjoint_domain_of_exists