Theorem Submodule.closure_eq'

Modification history

2026-01-17 20:29
Mathlib/Topology/Algebra/Module/ClosedSubmodule.lean
feat(Analysis/InnerProductSpace/Orthogonal): add duplicates for `ClosedSubmodule` (#29241) …
Added Submodule.closure_eq'View on Github →