Theorem Submodule.projectionL_eq_self_iff

Modification history

2026-06-25 07:54
Mathlib/Topology/Algebra/Module/Complement.lean
chore: remove unused instances (#41013) …
Modified Submodule.projectionL_eq_self_iffView on Github →
2026-06-10 10:22
Mathlib/Topology/Algebra/Module/Complement.lean
refactor(Analysis/Normed/Module/Complemented): add `IsCompl.isTopCompl_of_isClosed` and `isTopCompl_iff_isCompl_isClosed` (#39815) …
Modified Submodule.projectionL_eq_self_iffView on Github →
2026-05-05 09:37
Mathlib/Topology/Algebra/Module/Complement.lean
feat: define Submodule.IsTopCompl (#38547) …
Added Submodule.projectionL_eq_self_iffView on Github →