Skip to content

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

Closed
grunweg wants to merge 1 commit into
leanprover-community:masterfrom
grunweg:missing-38970
Closed

[Merged by Bors] - fix: correct deprecation for orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero#40722
grunweg wants to merge 1 commit into
leanprover-community:masterfrom
grunweg:missing-38970

fix: correct deprecation for orthogonalProjection_mem_subspace_orthog…

4dddbc9
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
check_title
succeeded Jun 17, 2026 in 1m 45s