search

jjdishere / EG

Formalizing Euclidean Geometry in Lean
26 stars 57 forks source link

define and prove properties of orthocenters with vector algebra #294

Open tonyxty opened 5 months ago

tonyxty commented 5 months ago

The definition might not be "geometric" enough but takes care of all corner cases.

Even if we decide upon another definition later, this lemma should still be useful.