Commit 2025-03-13 05:16 3d3450d0

View on Github →

feat: improve definition of AffineSubspace.mk', and use it in perpBisector (#22862) I replaced { q | ∃ v ∈ direction, q = v +ᵥ p } by { q | q -ᵥ p ∈ direction }. This definition is shorter and nicer to work with. I then use this to define perpBisector more conveniently. (And this removes one erw)

Estimated changes