Theorem Submodule.orthogonal_closure

Modification history

2025-06-10 14:32

Mathlib/Analysis/InnerProductSpace/Orthogonal.lean

feat(Analysis/InnerProductSpace): exchange range + ker (#25417) …

Added Submodule.orthogonal_closure View on Github →