Theorem LinearPMap.graph_adjoint_toLinearPMap_eq_adjoint

Modification history

2023-10-17 14:33
Mathlib/Analysis/InnerProductSpace/LinearPMap.lean
Revert "chore: revert #7703 (#7710)" …
Deleted LinearPMap.graph_adjoint_toLinearPMap_eq_adjointView on Github →
2023-10-16 19:01
Mathlib/Analysis/InnerProductSpace/LinearPMap.lean
chore: revert #7703 (#7710) …
Added LinearPMap.graph_adjoint_toLinearPMap_eq_adjointView on Github →
2023-10-16 04:14
Mathlib/Analysis/InnerProductSpace/LinearPMap.lean
chore: bump toolchain to v4.2.0-rc2 (#7703) …
Deleted LinearPMap.graph_adjoint_toLinearPMap_eq_adjointView on Github →
2023-10-16 02:18
Mathlib/Analysis/InnerProductSpace/LinearPMap.lean
feat(Analysis/InnerProductSpace/LinearPMap): the adjoint is closed (#6537) …
Added LinearPMap.graph_adjoint_toLinearPMap_eq_adjointView on Github →