Theorem Submodule.IsCompl.isTopCompl_of_isClosed_of_finiteDimensional

Modification history

2026-05-10 22:54
Mathlib/Topology/Algebra/Module/FiniteDimension.lean
feat: generalize Submodule.ClosedComplemented.of_quotient_finiteDimensional (#38579) …
Added Submodule.IsCompl.isTopCompl_of_isClosed_of_finiteDimensionalView on Github →