Theorem ClosedSubmodule.orthogonal_toSubmodule_eq

Modification history

2026-01-27 22:28
Mathlib/Analysis/InnerProductSpace/Orthogonal.lean
chore(Analysis/InnerProductSpace/Orthogonal): add simp attrib, rename (#34103) …
Deleted ClosedSubmodule.orthogonal_toSubmodule_eqView on Github →
2026-01-17 20:29
Mathlib/Analysis/InnerProductSpace/Orthogonal.lean
feat(Analysis/InnerProductSpace/Orthogonal): add duplicates for `ClosedSubmodule` (#29241) …
Added ClosedSubmodule.orthogonal_toSubmodule_eqView on Github →