Commit 2024-05-28 11:56 87543dce

feat(RingTheory/RootsOfUnity): product representation of the order of a primitive root of unity (#13290) This

• weakens the assumptions in X_pow_sub_C_eq_prod on the coefficient ring from "field" to "integral domain", and
• adds results on representing the order n of a primitive root of unity μ in R as a product involving terms like μ^k - 1. (In a new file RingTheory.RootsOfUnity.Lemmas because of fairly heavy imports.) This will be useful for results on Jacobi sums (to be added eventually).