Theorem Submodule.ClosedComplemented.of_finiteDimensional

Modification history

2023-12-03 09:54
Mathlib/Analysis/NormedSpace/HahnBanach/Extension.lean
feat(Analysis/HahnBanach): extension of a CLM with finite dimensional range (#8604) …
Added Submodule.ClosedComplemented.of_finiteDimensionalView on Github →