Zulip Chat Archive
Stream: Is there code for X?
Topic: nat-bezout
Eric Rodriguez (Jan 13 2022 at 13:03):
do we have the statement that if a.coprime b, then there exists k l : nat with ak + bl = 1 mod (a/b)? I don't mind the stronger gcd statement but this is good enough for me
Eric Rodriguez (Jan 13 2022 at 13:04):
i'd rather not go to int because then i have to start messing with zpow (i'm proving that the (1 - zeta^k) are all associated to each other)
Riccardo Brasca (Jan 13 2022 at 13:04):
This is the definition of docs#is_coprime
Riccardo Brasca (Jan 13 2022 at 13:05):
Wait, it is false if you want everything in N, isn't it?
Yaël Dillies (Jan 13 2022 at 13:06):
mod a and mod b
Riccardo Brasca (Jan 13 2022 at 13:07):
I think I don't understand the exact question, what does mod (a/b) mean?
Yaël Dillies (Jan 13 2022 at 13:10):
What I just said, I assume
Eric Rodriguez (Jan 13 2022 at 13:13):
I meant mod either , but I was using nat.coprime
Eric Rodriguez (Jan 13 2022 at 13:13):
There's probably some compatibility lemmas though, thanks!
Floris van Doorn (Jan 13 2022 at 13:14):
There is some stuff on docs#pnat, like docs#pnat.gcd_rel_left.
Riccardo Brasca (Jan 13 2022 at 13:14):
I see. In that case I would try to use chinese remainder theorem to work modulo a * b.
Riccardo Brasca (Jan 13 2022 at 13:15):
Sorry, I keep thinking about integers
Riccardo Brasca (Jan 13 2022 at 13:16):
If you are doing this for flt-regular maybe the best thing is to go to the units group, so integer powers are not a problem.
Eric Rodriguez (Jan 13 2022 at 13:29):
this is for proving that these things are in the units group ;b I'll check that out, thanks Floris!
Eric Rodriguez (Jan 13 2022 at 13:30):
(the is_coprime connection is through the int cast sadly)
Eric Rodriguez (Jan 13 2022 at 13:33):
ah, it is there! in data/int/gcd, we have docs#nat.exists_mul_mod_eq_one_of_coprime. thanks!
Alex J. Best (Jan 13 2022 at 13:44):
What happened to the old definition of cyclotomic_unit we had?
Alex J. Best (Jan 13 2022 at 13:46):
Oh it was deleted in 5dc5d5c9a91a6f0ac89e0a478e853a9641596f91
Eric Rodriguez (Jan 13 2022 at 13:49):
yeah i broke it in the zeta refactor and i was trying to restart it
Eric Rodriguez (Jan 13 2022 at 13:49):
i think this question is what aux was
Alex J. Best (Jan 13 2022 at 13:55):
Yeah I think that mathlib declaration is pretty much what I wanted, but a def rather than exists
Eric Rodriguez (Jan 13 2022 at 13:56):
ahh, so it could be done constructively?
Alex J. Best (Jan 13 2022 at 13:57):
Yeah not that it matters too much, its just seems a bit odd to have to use choice to invert something mod a prime
Eric Rodriguez (Jan 13 2022 at 13:57):
i guess mul_mod_eq_gcd gives the exact number
Alex J. Best (Jan 13 2022 at 13:58):
Is that a def somewhere?
Eric Rodriguez (Jan 13 2022 at 13:59):
it's the statement above it which it uses in the proof, it has a refine step with the explicit number
Alex J. Best (Jan 13 2022 at 14:07):
Oh right yes thats exactly the same as what I had defined aux, I guess there is only one obvious choice!
Eric Rodriguez (Jan 13 2022 at 14:35):
I just pushed an updated version, feel free to toy around with it^^ sorry for breaking it in the first place!
Alex J. Best (Jan 13 2022 at 14:52):
No need to apologize, I was just confused where it was lol :smile: its my bad for writing such half-baked code :grinning:
Last updated: Dec 20 2023 at 11:08 UTC