Galois fields or Elliptic curves?

Stream: Is there code for X?

[SnowFox]

Hello world. I see mathlib has field, zmod and poly; but AFAICT does not have the common Galois Field extensions. I.e. Powers of primes and binary specializations. I'd like to implement ed25519 and ed448; and the ristretto255 and 448 groups on top of these. Have I missed anything relevant in mathlib? Can someone give me a push for how I should continue? Thank you in advance.

[Johan Commelin]

@SnowFox That's about right. There is a branch finite-fields trying to implement the other Galois fields, but it has been dormant for a while.

[Johan Commelin]

But recently we've had a lot of new stuff about separable extensions and such, so it should be rather easy to get those fields working now.

[Johan Commelin]

About two months ago, some people defined the group law on Weierstrass elliptic curves, but I don't think anyone has done edwards curves.

[SnowFox]

Thanks @Johan Commelin . Did you mean the finite-fields-exist branch? I'll need to poke around the branches.. many! :)

[Johan Commelin]

@SnowFox My bad, that must have been the branch name.