Mathlib v3 is deprecated. Go to Mathlib v4

Theorem orthogonal_family.submodule_is_internal_iff

Modification history

2022-05-24 14:54
src/analysis/inner_product_space/projection.lean
refactor(algebra/direct_sum/basic): use the new polymorphic subobject API (#14341) …
Deleted orthogonal_family.submodule_is_internal_iffView on Github →
2021-11-12 20:02
src/analysis/inner_product_space/projection.lean
feat(analysis/inner_product_space/spectrum): diagonalization of self-adjoint endomorphisms (finite dimension) (#9995) …
Modified orthogonal_family.submodule_is_internal_iffView on Github →
2021-10-21 15:43
src/analysis/inner_product_space/projection.lean
feat(analysis/inner_product_space): define `orthogonal_family` of subspaces (#9718) …
Added orthogonal_family.submodule_is_internal_iffView on Github →