Theorem ClosedSubmodule.mem_orthogonal_toSubmodule_iff

Modification history

2026-01-27 22:28
Mathlib/Analysis/InnerProductSpace/Orthogonal.lean
chore(Analysis/InnerProductSpace/Orthogonal): add simp attrib, rename (#34103) …
Added ClosedSubmodule.mem_orthogonal_toSubmodule_iffView on Github →