feat(ring_theory/roots_of_unity): Restrict ring homomorphism to roots of unity (#6646)
feat(ring_theory/roots_of_unity): Restrict ring homomorphism to roots of unity (#6646)

Restrict a ring homomorphism to roots of unity.



Co-authored-by: tb65536 <25c750517795e47f172dc8c552ed72c7de260bd4@users.noreply.github.com>

leanprover-community/mathlib,leanprover-community/mathlib