Riccardo Brasca
Riccardo Brasca
Can you please fix the conflict?
> Thanks for the reviews! I'll get back to this PR in 1-2 days. Feel free to commit directly in the meantime. @alreadydone I've added `awaiting author` and removed `awaiting...
Can you please merge master to see if it still works?
This looks good to me. @kbuzzard @AlexKontorovich can you have a look?
> Should we call this `map`? I was expecting this to be the fact that two n-th cyclotomic extensions were equivalent, which is something I don't think we actually yet...
> > Should we call this `map`? I was expecting this to be the fact that two n-th cyclotomic extensions were equivalent, which is something I don't think we actually...
> oh, nice! do you know if it works in the general infinite case? if you don't, I may have a think about it for fun soon. We should first...
I've added the lemmas needed to use `trans` to prove `equiv`, but unfortunately `trans` has additional assumptions (especially `no_zero_smul_divisors B C`, that is really needed) that are not needed for...
> I've added the lemmas needed to use `trans` to prove `equiv`, but unfortunately `trans` has additional assumptions (especially `no_zero_smul_divisors B C`, that is really needed) that are not needed...