Commit 2024-03-18 09:20 93867128

feat: add mod n cyclotomic character (#6342) We define the group homomorphism Aut(L)->(Z/dZ)^* coming from the action on the n'th roots of unity in L. Here d is the number of n'th roots of unity in L (which might not be n in this generality). We also make API for the standard special case when there are n n'th roots of unity in L, calling it ModularCyclotomicCharacter. Joint work with Hanneke Wiersema, coming from the Leiden conference on machine checked mathematics.