Theorem Submodule.IsCompl.isTopCompl_of_finiteDimensional_quotient

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_finiteDimensional_quotientView on Github →