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
)