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)