Commit 2025-12-16 10:54 9ead4967

View on Github →

chore(Analysis/InnerProductSpace): remove a redundant CompleteSpace assumption (#32926)

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Projection/Submodule.lean

modified theorem Submodule.triorthogonal_eq_orthogonal