Theorem ClosedSubmodule.toSubmodule_orthogonal_eq

Modification history

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