issues
search
jjdishere
/
EG
Formalizing Euclidean Geometry in Lean
26
stars
57
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Updated Tactic Congruence
#303
xyzw12345
closed
3 months ago
0
Orthocenter construction
#302
Yu-Misaka
closed
4 months ago
0
Complete the part of Position/Angle and problem 2 of IMO in 2007
#301
mbkybky
closed
4 months ago
0
added Linear.Order
#300
xyzw12345
closed
5 months ago
0
implicit parameters in iff lemma
#299
FR-vdash-bot
closed
5 months ago
0
Axiom/Circle
#298
Noaillesss
closed
5 months ago
0
`Type _` -> `Type*`
#297
FR-vdash-bot
closed
5 months ago
2
`collinear` -> `Collinear` & `parallel` -> `Parallel` & `perpendicular` -> `Perpendicular` & other name changes
#296
FR-vdash-bot
closed
5 months ago
0
redefine collinear & lemmas & naming
#295
FR-vdash-bot
opened
5 months ago
0
define and prove properties of orthocenters with vector algebra
#294
tonyxty
opened
5 months ago
0
Adding description of theorems in parallel.lean and perpendicular.lean
#293
Liang-Xiao-pku
closed
5 months ago
0
Fill all sorries in Ray.lean and a sorry in Line.lean
#292
Origami233333
closed
5 months ago
0
finish ray ray intersect in the plan
#291
Thmoas-Guan
closed
5 months ago
1
prove perpendicular from inner product zero
#290
tonyxty
closed
5 months ago
0
Update ShanZun Ex1f'
#289
stupidchunchun
closed
5 months ago
0
Update Position/Angle and clean trash in Linear and Position/Angle
#288
mbkybky
closed
5 months ago
0
colinear -> collinear
#287
FR-vdash-bot
closed
5 months ago
0
修改了ShanZun Ex1f‘ 和 Ray.trash
#286
stupidchunchun
closed
5 months ago
0
add compatibility of seg and relative side
#285
Thmoas-Guan
closed
5 months ago
0
Team_D_changed_Parallelogram.lean&Quadrilateral.lean
#284
kfc2333
closed
5 months ago
2
对Example ShanZun ex1f 中的2.11做了尝试性的修改
#283
stupidchunchun
closed
5 months ago
0
Complete Position/Angle.lean and Clean trash of Ray.lean
#282
mbkybky
closed
5 months ago
0
fix the problem left
#281
Thmoas-Guan
closed
5 months ago
0
add some little theorems in orientation
#280
Thmoas-Guan
closed
5 months ago
0
Axiom/Circle
#279
Noaillesss
closed
5 months ago
0
fix the silly theorem of cclock and angle pos
#278
Thmoas-Guan
closed
5 months ago
0
point reflection
#277
Noaillesss
opened
5 months ago
0
some updates on anglebisector
#276
XintaoYu
closed
5 months ago
0
Fix errors
#275
mbkybky
closed
5 months ago
0
Update AddToMathlib.lean, Vector.lean, Line.lean and Position/Angle.lean
#274
mbkybky
closed
5 months ago
0
Axiom/Circle
#273
Noaillesss
closed
5 months ago
0
Congruence exercise ygr 1-4
#272
Thmoas-Guan
closed
5 months ago
0
Some refinement of Ray.lean, Line.lean, Triangle.lean, Similarity.lean and so on
#271
mbkybky
closed
6 months ago
0
Schaum Problem1.5 1.6 1.7 1.8 1.9
#270
xyzw12345
closed
6 months ago
3
Use PtNe everywhere
#269
jjdishere
opened
6 months ago
0
More instance of PtNe
#268
jjdishere
opened
6 months ago
1
Complement of Similarity.lean
#267
2200010613
closed
6 months ago
0
Update Basic/Angle.lean
#266
mbkybky
closed
6 months ago
0
Axiom/Circle
#265
Noaillesss
closed
6 months ago
0
Team_D_changed_Parallelogram.lean&Quadrilateral.lean
#264
kfc2333
closed
6 months ago
0
use `PtNe` typeclass in lemmas
#263
FR-vdash-bot
closed
6 months ago
0
bundled ceva configuration
#262
FR-vdash-bot
closed
6 months ago
0
Add_files_EX1c'.lean,EX1e'.lean,EX1h'.lean,Chap5a.lean_Modified_the_style_of_examples
#261
mathzhuonichi
closed
6 months ago
0
`PtNe` typeclass and let the notations use it automatically
#260
FR-vdash-bot
closed
6 months ago
0
Update Basic/Angle.lean
#259
mbkybky
closed
6 months ago
0
修改了一些定理名字问题，增加了几个题
#258
stupidchunchun
closed
6 months ago
0
IsROrC typeclasses and more lemmas about cdiv
#257
FR-vdash-bot
closed
6 months ago
0
Reorganizing lemmas about angles and linear maps
#256
FR-vdash-bot
closed
6 months ago
0
Fill some sorry in Basic/Angle.lean
#255
mbkybky
closed
6 months ago
0
notation for `Real -> AngValue`
#254
FR-vdash-bot
closed
6 months ago
0
Next