Orthogonality

📁 Source: Mathlib/NumberTheory/DirichletCharacter/Orthogonality.lean

Statistics

Metric	Count
Definitions fintype	1
Theorems card_eq_totient_of_hasEnoughRootsOfUnity, exists_apply_ne_one_of_hasEnoughRootsOfUnity, mulEquiv_units, sum_char_inv_mul_char_eq, sum_characters_eq, sum_characters_eq_zero	6
Total	7

DirichletCharacter

Definitions

Name	Category	Theorems
fintype 📖	CompOp	6 math math: ArithmeticFunction.vonMangoldt.residueClass_eq, sum_characters_eq, ArithmeticFunction.vonMangoldt.residueClass_apply, sum_char_inv_mul_char_eq, sum_characters_eq_zero, ArithmeticFunction.vonMangoldt.LSeries_residueClass_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_eq_totient_of_hasEnoughRootsOfUnity 📖	mathematical	—	Nat.card DirichletCharacter CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring Nat.totient	—	ZMod.card_units_eq_totient Nat.card_eq_fintype_card Nat.card_congr mulEquiv_units
exists_apply_ne_one_of_hasEnoughRootsOfUnity 📖	—	—	—	—	MulChar.exists_apply_ne_one_of_hasEnoughRootsOfUnity Finite.of_fintype
mulEquiv_units 📖	mathematical	—	MulEquiv DirichletCharacter CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring Units ZMod MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring ZMod.commRing MulChar.hasMul CommRing.toCommMonoid Units.instMul	—	MulChar.mulEquiv_units Finite.of_fintype
sum_char_inv_mul_char_eq 📖	mathematical	IsUnit ZMod MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing	Finset.sum DirichletCharacter CommSemiring.toCommMonoidWithZero NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finset.univ fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib DFunLike.coe MulChar.instFunLike CommRing.toCommMonoid ZMod.instInv ZMod.decidableEq AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.totient MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Finset.sum_congr MonoidHomClass.toMulHomClass MulCharClass.toMonoidHomClass MulChar.instMulCharClass sum_characters_eq ZMod.inv_mul_eq_one_of_isUnit
sum_characters_eq 📖	mathematical	—	Finset.sum DirichletCharacter CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finset.univ fintype DFunLike.coe ZMod MulChar.instFunLike CommRing.toCommMonoid ZMod.commRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing ZMod.decidableEq AddMonoidWithOne.toNatCast Nat.totient MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Finset.sum_congr map_one MonoidHomClass.toOneHomClass MulCharClass.toMonoidHomClass MulChar.instMulCharClass Finset.sum_const nsmul_eq_mul mul_one card_eq_totient_of_hasEnoughRootsOfUnity sum_characters_eq_zero
sum_characters_eq_zero 📖	mathematical	—	Finset.sum DirichletCharacter CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finset.univ fintype DFunLike.coe ZMod MulChar.instFunLike CommRing.toCommMonoid ZMod.commRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	exists_apply_ne_one_of_hasEnoughRootsOfUnity IsDomain.toNontrivial eq_zero_of_mul_eq_self_left IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero Finset.mul_sum Finset.sum_congr Fintype.sum_bijective Group.mulLeft_bijective

---

← Back to Index