Commit 2024-02-24 17:22 cf963957

View on Github →

fix(RingTheory/RootsOfUnity/Basic): generalise some results to monoids (#10605) These results are all proved for commutative semirings but all work for commutative monoids.

Estimated changes

Modified Mathlib/RingTheory/RootsOfUnity/Basic.lean

added theorem MulEquiv.restrictRootsOfUnity_coe_apply

added theorem MulEquiv.restrictRootsOfUnity_symm

deleted theorem RingEquiv.restrictRootsOfUnity_coe_apply

deleted theorem RingEquiv.restrictRootsOfUnity_symm

modified def restrictRootsOfUnity

modified theorem restrictRootsOfUnity_coe_apply