mathlib3
feat(geometry/euclidean/ceva) : Ceva's Theorem, problem 61 on Freek's list
#10632
Open
Open
feat(geometry/euclidean/ceva) : Ceva's Theorem, problem 61 on Freek's list #10632
MantasBaksys
wants to merge
22 commits into
master
from
ceva-theorem
initial lemma
068c8e0f
update
0880fdd0
Update Ceva's Theorem.lean
e3dcb007
Update Ceva's Theorem.lean
faa305a2
update
86bc259e
Update ceva_theorem.lean
f4a80815
Merge branch 'master' of https://github.com/leanprover-community/math…
9179fcbe
bump mathlib and refactor
93a5b582
finish permutation proof
43bd0b2b
Update ceva_theorem.lean
d010bff6
full proof
755fca4b
proof golf + docstring
9b019829
fix docstring
06467ef2
jcommelin
changed the title
jsm28
commented
on 2021-12-14
jsm28
commented
on 2021-12-14
jsm28
commented
on 2021-12-14
jsm28
commented
on 2021-12-14
jsm28
commented
on 2021-12-14
Merge remote-tracking branch 'origin/master' into ceva-theorem
9beb7907
rename
8ee725f6
golf, reduce assumptions
8bba30e8
move affine_basis.interior_coord_pos, update 100.yaml
5aaec111
YaelDillies
changed the title
Merge remote-tracking branch 'origin/master' into ceva-theorem
b95feb6f
affine_basis.reindex API
9ed4cf25
Merge remote-tracking branch 'origin/master' into ceva-theorem
2a9ad730
reduce diff
0d2d7904
bump
ae845de1
Reviewers
Assignees
No one assigned
Labels
awaiting-review
t-euclidean-geometry
too-late
Milestone
No milestone
Login to write a write a comment.
Login via GitHub