Theorem ClosedSubmodule.orthogonal_orthogonal_monotone

Modification history

2026-01-17 20:29

Mathlib/Analysis/InnerProductSpace/Orthogonal.lean

feat(Analysis/InnerProductSpace/Orthogonal): add duplicates for `ClosedSubmodule` (#29241) …

Added ClosedSubmodule.orthogonal_orthogonal_monotone View on Github →