Zulip Chat Archive

Stream: new members

Topic: Ceva theorem, first try


Anders Larsson (Jan 05 2022 at 01:32):

I have tried to adapt the Ceva theorem proof from Metamath.

Available at: https://gist.github.com/anders-was-here/d786450daba4c01e40bbc5f81c681feb

Original proof/formalization by Saveliy Skresanov: http://us.metamath.org/mpeuni/cevath.html

Arthur Paulino (Jan 05 2022 at 01:39):

I really like the font you used in some comments btw. I think this is the first time I see it

Anders Larsson (Jan 05 2022 at 01:42):

Arthur Paulino said:

I really like the font you used in some comments btw. I think this is the first time I see it

It must be unicode. (I think Gists are pure text files). It's cut'n'paste from the Metamath page.

Yaël Dillies (Jan 05 2022 at 08:10):

Congrats! Have a look at #10632 and a chat with @Mantas Baksys


Last updated: Dec 20 2023 at 11:08 UTC