[Merged by Bors] - fix: correct deprecation for orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero - #40722

[Merged by Bors] - fix: correct deprecation for orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero#40722

grunweg wants to merge 1 commit into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

grunweg:missing-38970grunweg/mathlib4:missing-38970Copy head branch name to clipboard