feat(Crypto/Systems): Elligator 1, Theorem 1 and Definition 2 - #783

Open

chris-anto-froeschl wants to merge 5 commits into

leanprover:mainfrom

chris-anto-froeschl:elligator1

Commits on Aug 8, 2026

adds Elligator 1 theorem 1 and definition 2, adds bibliography entry for bernstein2013a, updates Cslib.lean to include new files
chris-anto-froeschl
committed
c4b88f8
adds import of Cslib.Init in Crypto/Systems/Elligator/Basic.lean
chris-anto-froeschl
committed
dbaaf17

Commits on Aug 16, 2026

fixes indent of statements and proofs, removes trivial lemmas
chris-anto-froeschl
committed
30a853b
Merge branch 'main' into elligator1
chris-anto-froeschl
committed
f8fc18f
adds Cslib.Init import to TwistedEdwardsCurve.lean
chris-anto-froeschl
committed
e36c1bd