Mathlib v3 is deprecated. Go to Mathlib v4

Theorem submodule.adjoint_orthogonal_projection

Modification history

2022-07-23 22:32
src/analysis/inner_product_space/adjoint.lean
feat(analysis/inner_product_space/positive): definition and basic facts about positive operators (#15470)
Added submodule.adjoint_orthogonal_projectionView on Github →