## Stream: Is there code for X?

### Topic: Galois fields or Elliptic curves?

#### SnowFox (Sep 01 2020 at 10:23):

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 (Sep 01 2020 at 10:59):

@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 (Sep 01 2020 at 10:59):

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 (Sep 01 2020 at 11:00):

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 (Sep 01 2020 at 12:05):

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

#### Johan Commelin (Sep 01 2020 at 12:14):

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

Last updated: May 19 2021 at 00:40 UTC