Commit 2024-11-07 08:51 3066cf46

View on Github →

feat: duality results for cyclic groups (#18687) This PR adds orthogonality results for cyclic groups (point 1 in this message on Zulip).

Estimated changes

Modified Mathlib/RingTheory/RootsOfUnity/Basic.lean

added def IsCyclic.monoidHomMulEquivRootsOfUnityOfGenerator

added theorem IsCyclic.monoidHom_mulEquiv_rootsOfUnity

Modified Mathlib/RingTheory/RootsOfUnity/EnoughRootsOfUnity.lean

added theorem monoidHom_equiv_self

Modified Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean

added theorem IsCyclic.exists_apply_ne_one

added theorem ZMod.exists_monoidHom_apply_ne_one