Commit 2024-11-09 11:53 5476cef7

View on Github →

feat(NumberTheory/DirichletCharacter/Orthogonality): new file (#18777) This PR is the final step in establishing the orthogonality relations for Dirichlet characters. See here on Zulip.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/ZMod/Basic.lean

added theorem ZMod.inv_mul_eq_one_of_isUnit

Modified Mathlib/GroupTheory/FiniteAbelian/Duality.lean

added theorem CommGroup.monoidHom_mulEquiv_of_hasEnoughRootsOfUnity

deleted theorem CommGroup.mulEquiv_monoidHom_of_hasEnoughRootsOfUnity

Created Mathlib/NumberTheory/DirichletCharacter/Orthogonality.lean

added theorem DirichletCharacter.card_eq_totient_of_hasEnoughRootsOfUnity

added theorem DirichletCharacter.exists_apply_ne_one_of_hasEnoughRootsOfUnity

added theorem DirichletCharacter.mulEquiv_units

added theorem DirichletCharacter.sum_char_inv_mul_char_eq

added theorem DirichletCharacter.sum_characters_eq

added theorem DirichletCharacter.sum_characters_eq_zero

Modified Mathlib/NumberTheory/MulChar/Duality.lean