Commit 2025-05-18 20:46 ddbcd9d9
View on Github →feat: add a congruence lemma for orthogonalProjection (#25004)
While it is still tricky to rewrite with rw, this makes it work with simp.
feat: add a congruence lemma for orthogonalProjection (#25004)
While it is still tricky to rewrite with rw, this makes it work with simp.