search

jjdishere / EG

Formalizing Euclidean Geometry in Lean
28 stars 56 forks source link

Split Vector.lean #69

Open jjdishere opened 1 year ago

jjdishere commented 1 year ago

Should split Dir Proj to another file

jjdishere commented 1 year ago

for all new theorems adders, please be careful where a theorem should belong. We should organize theorems in the way of logic dependency, not time/author/aim

jjdishere commented 1 year ago

More linear algebra is incoming. Discussing >0 of det and cu cv.