roots of unity

Stream: mathlib4

[Kevin Buzzard]

In RingTheory.RootsOfUnity.Basic I am amused to note that after the initial rootsOfUnity section (initial lemmas, valid for CommMonoids) there is a CommSemiring section (lines 134 to 179) and the lemmas there also all work fine for CommMonoids :-) What is the reason that they are proved for CommSemirings? Could there be a justification for this? For example 99% of the time they're applied to RingHoms and people don't want to write .toMulHom?

[Ruben Van de Velde]

Is there a reason they're not proved for MonoidHomClass?

[Riccardo Brasca]

I am pretty sure this is just some sort of historical accident. Feel free to PR any generalization :)

[Jireh Loreaux]

Kevin, we shouldn't be writing .toMulHom, we have coercions for that sort of thing.

[Kevin Buzzard]

#10605 let's see if anything breaks.