Mathlib Changelog
v4
Changelog
About
Github
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