search

jjdishere / EG

Formalizing Euclidean Geometry in Lean
26 stars 57 forks source link

Update ShanZun Ex1f' #289

Closed stupidchunchun closed 5 months ago

stupidchunchun commented 5 months ago

将原来的Ex1F文件全部转化为了现在需要的格式，并补充了一些证明，剩下的sorry是一些当时没有写证明的整个题目的完整的证明，还有PtNe证明，notColinear证明，还有一些跟LinearOrder相关的证明（比如我微信问学长的问题）