Zulip Chat Archive
Stream: Is there code for X?
Topic: Extended Euclidean Algorithm
Adam Topaz (Sep 06 2023 at 16:31):
Do we have the extended Euclidean algorithm somewhere?
Eric Rodriguez (Sep 06 2023 at 16:40):
Eric Rodriguez (Sep 06 2023 at 16:40):
ok it's nat.xgcd
Eric Rodriguez (Sep 06 2023 at 16:40):
let's see if it survived lean4 renaming
Eric Rodriguez (Sep 06 2023 at 16:41):
Adam Topaz (Sep 06 2023 at 16:42):
Perfect, thanks!
Antoine Chambert-Loir (Sep 07 2023 at 16:45):
Isn't there an xgcd for rings with given euclidean division? And it is strange that docs#Int.xgcd resorts to the Nat version after taking absolute values.
Anatole Dedecker (Sep 07 2023 at 16:47):
I think it would be fun to implement the Smith normal form algorithm and deducexgcd as a particular case.
Anatole Dedecker (Sep 07 2023 at 16:47):
But I don't think we have any of that.
Anatole Dedecker (Sep 07 2023 at 16:53):
Although if we end up having that I'm going to get very sad that polynomials are noncomputable...
Eric Rodriguez (Sep 07 2023 at 17:00):
Anatole Dedecker (Sep 07 2023 at 17:12):
Oh I didn't know about that. There's still no concrete algorithm right? By the way, everything about docs#Basis.SmithNormalForm could be generalized to any linear map between free modules instead of the inclusion from a submodule, right?
Eric Rodriguez (Sep 07 2023 at 17:30):
cc @Oliver Nash, who wrote the new lemmas. Anne wrote the original code, but I don't want to ping them mid-PhD writing!
Last updated: Dec 20 2023 at 11:08 UTC