Basic

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

Statistics

Metric	Count
Definitions DirichletCharacter, χ₀, IsPrimitive, changeLevel, conductor, conductorSet, instUniqueOfNatNat, mul, primitiveCharacter, primitive_mul	10
Theorems eval_neg, not_odd, toUnitHom_eval_neg_one, to_fun, dvd, eq_changeLevel, existsUnique, same_level, eval_neg, not_even, toUnitHom_eval_neg_one, to_fun, changeLevel_def, changeLevel_eq_cast_of_dvd, changeLevel_eq_one_iff, changeLevel_factorsThrough, changeLevel_injective, changeLevel_one, changeLevel_primitiveCharacter, changeLevel_self, changeLevel_self_toUnitHom, changeLevel_toUnitHom, changeLevel_trans, conductor_dvd_level, conductor_dvd_of_mem_conductorSet, conductor_eq_zero_iff_level_eq_zero, conductor_le_conductor_mem_conductorSet, conductor_mem_conductorSet, conductor_ne_zero, conductor_one, conductor_one_dvd, eq_one_iff_conductor_eq_one, eval_modulus_sub, even_or_odd, factorsThrough_conductor, factorsThrough_gcd, factorsThrough_iff_ker_unitsMap, factorsThrough_one_iff, instSubsingletonOfNatNat, isPrimitive_def, isPrimitive_one_level_one, isPrimitive_one_level_zero, level_mem_conductorSet, level_one, level_one', map_zero', mem_conductorSet_dvd, mem_conductorSet_iff, mul_def, not_even_and_odd, primitiveCharacter_isPrimitive, primitiveCharacter_one, primitive_mul_isPrimitive, toUnitHom_eq_char', toUnitHom_inj, zero_ne_mem_conductorSet	56
Total	66

DirichletCharacter

Definitions

Name	Category	Theorems
IsPrimitive 📖	MathDef	5 math math: isPrimitive_def, primitiveCharacter_isPrimitive, primitive_mul_isPrimitive, isPrimitive_one_level_one, isPrimitive_one_level_zero
changeLevel 📖	CompOp	16 math math: changeLevel_injective, changeLevel_def, conductor_le_conductor_mem_conductorSet, changeLevel_trans, LFunction_changeLevel, LSeries_changeLevel, changeLevel_one, changeLevel_toUnitHom, changeLevel_factorsThrough, changeLevel_eq_one_iff, FactorsThrough.existsUnique, changeLevel_self_toUnitHom, changeLevel_primitiveCharacter, changeLevel_self, changeLevel_eq_cast_of_dvd, FactorsThrough.eq_changeLevel
conductor 📖	CompOp	14 math math: conductor_le_conductor_mem_conductorSet, isPrimitive_def, primitiveCharacter_one, conductor_dvd_level, conductor_one, primitiveCharacter_isPrimitive, conductor_mem_conductorSet, primitive_mul_isPrimitive, eq_one_iff_conductor_eq_one, conductor_eq_zero_iff_level_eq_zero, conductor_dvd_of_mem_conductorSet, factorsThrough_conductor, changeLevel_primitiveCharacter, conductor_one_dvd
conductorSet 📖	CompOp	4 math math: conductor_mem_conductorSet, level_mem_conductorSet, mem_conductorSet_iff, zero_ne_mem_conductorSet
instUniqueOfNatNat 📖	CompOp	—
mul 📖	CompOp	2 math math: primitive_mul_isPrimitive, mul_def
primitiveCharacter 📖	CompOp	4 math math: primitiveCharacter_one, primitiveCharacter_isPrimitive, mul_def, changeLevel_primitiveCharacter
primitive_mul 📖	CompOp	2 math math: primitive_mul_isPrimitive, mul_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
changeLevel_def 📖	mathematical	—	DFunLike.coe MonoidHom DirichletCharacter MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup MulChar.commGroup ZMod CommRing.toCommMonoid ZMod.commRing MonoidHom.instFunLike changeLevel MulChar.ofUnitHom MonoidHom.comp Units CommMonoid.toMonoid MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero Units.instMulOneClass MulChar.toUnitHom ZMod.unitsMap	—	—
changeLevel_eq_cast_of_dvd 📖	mathematical	—	DFunLike.coe DirichletCharacter ZMod MulChar.instFunLike CommRing.toCommMonoid ZMod.commRing MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup MulChar.commGroup MonoidHom.instFunLike changeLevel Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring ZMod.cast Ring.toAddGroupWithOne CommRing.toRing	—	MulChar.equivToUnitHom_symm_coe MulChar.coe_equivToUnitHom
changeLevel_eq_one_iff 📖	mathematical	—	DFunLike.coe MonoidHom DirichletCharacter MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup MulChar.commGroup ZMod CommRing.toCommMonoid ZMod.commRing MonoidHom.instFunLike changeLevel MulChar.hasOne	—	map_eq_one_iff MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass changeLevel_injective
changeLevel_factorsThrough 📖	mathematical	—	FactorsThrough DFunLike.coe MonoidHom DirichletCharacter MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup MulChar.commGroup ZMod CommRing.toCommMonoid ZMod.commRing MonoidHom.instFunLike changeLevel	—	—
changeLevel_injective 📖	mathematical	—	DirichletCharacter DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup MulChar.commGroup ZMod CommRing.toCommMonoid ZMod.commRing MonoidHom.instFunLike changeLevel	—	MulChar.ext ZMod.unitsMap_surjective MulChar.equivToUnitHom_symm_coe MulChar.coe_equivToUnitHom MulChar.ext_iff
changeLevel_one 📖	mathematical	—	DFunLike.coe MonoidHom DirichletCharacter MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup MulChar.commGroup ZMod CommRing.toCommMonoid ZMod.commRing MonoidHom.instFunLike changeLevel MulChar.hasOne	—	map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass
changeLevel_primitiveCharacter 📖	mathematical	—	DFunLike.coe MonoidHom DirichletCharacter conductor MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup MulChar.commGroup ZMod CommRing.toCommMonoid ZMod.commRing MonoidHom.instFunLike changeLevel conductor_dvd_level primitiveCharacter	—	factorsThrough_conductor
changeLevel_self 📖	mathematical	—	DFunLike.coe MonoidHom DirichletCharacter MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup MulChar.commGroup ZMod CommRing.toCommMonoid ZMod.commRing MonoidHom.instFunLike changeLevel dvd_refl Nat.instMonoid	—	dvd_refl ZMod.charP MonoidHomClass.toMonoidHom.congr_simp ZMod.castHom_self Units.map_id MonoidHom.CompTriple.comp_eq MonoidHom.CompTriple.instComp_id MonoidHom.CompTriple.instIsId Equiv.symm_apply_apply
changeLevel_self_toUnitHom 📖	mathematical	—	MulChar.toUnitHom ZMod CommRing.toCommMonoid ZMod.commRing DFunLike.coe MonoidHom DirichletCharacter MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup MulChar.commGroup MonoidHom.instFunLike changeLevel dvd_refl Nat.instMonoid	—	dvd_refl changeLevel_self
changeLevel_toUnitHom 📖	mathematical	—	MulChar.toUnitHom ZMod CommRing.toCommMonoid ZMod.commRing DFunLike.coe MonoidHom DirichletCharacter MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup MulChar.commGroup MonoidHom.instFunLike changeLevel MonoidHom.comp Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring CommMonoid.toMonoid CommMonoidWithZero.toMonoidWithZero Units.instMulOneClass ZMod.unitsMap	—	Equiv.apply_symm_apply
changeLevel_trans 📖	mathematical	—	DFunLike.coe MonoidHom DirichletCharacter MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup MulChar.commGroup ZMod CommRing.toCommMonoid ZMod.commRing MonoidHom.instFunLike changeLevel dvd_trans Nat.instSemigroup	—	dvd_trans Equiv.apply_symm_apply ZMod.unitsMap_comp
conductor_dvd_level 📖	mathematical	—	conductor	—	FactorsThrough.dvd conductor_mem_conductorSet
conductor_dvd_of_mem_conductorSet 📖	mathematical	Set Set.instMembership conductorSet	conductor	—	Mathlib.Tactic.Contrapose.contrapose₃ zero_ne_mem_conductorSet conductor_ne_zero changeLevel_injective dvd_trans changeLevel_trans conductor_dvd_level changeLevel_primitiveCharacter factorsThrough_gcd Nat.sInf_le Mathlib.Tactic.Contrapose.contrapose₁ Iff.not
conductor_eq_zero_iff_level_eq_zero 📖	mathematical	—	conductor	—	Function.mtr conductor_ne_zero Nat.sInf_eq_zero level_mem_conductorSet
conductor_le_conductor_mem_conductorSet 📖	mathematical	Set Set.instMembership conductorSet	conductor DirichletCharacter DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup MulChar.commGroup ZMod CommRing.toCommMonoid ZMod.commRing MonoidHom.instFunLike changeLevel	—	Nat.sInf_le mem_conductorSet_iff dvd_trans conductor_dvd_level factorsThrough_conductor FactorsThrough.dvd changeLevel_trans FactorsThrough.eq_changeLevel
conductor_mem_conductorSet 📖	mathematical	—	Set Set.instMembership conductorSet conductor	—	Nat.sInf_mem Set.nonempty_of_mem level_mem_conductorSet
conductor_ne_zero 📖	—	—	—	—	conductor_dvd_level
conductor_one 📖	mathematical	—	conductor DirichletCharacter MulChar.hasOne ZMod CommRing.toCommMonoid ZMod.commRing	—	factorsThrough_one_iff Nat.sInf_le mem_conductorSet_iff conductor_ne_zero
conductor_one_dvd 📖	mathematical	—	conductor DirichletCharacter MulChar.hasOne ZMod CommRing.toCommMonoid ZMod.commRing	—	isPrimitive_def isPrimitive_one_level_one one_dvd
eq_one_iff_conductor_eq_one 📖	mathematical	—	DirichletCharacter MulChar.hasOne ZMod CommRing.toCommMonoid ZMod.commRing conductor	—	conductor_one factorsThrough_conductor level_one' changeLevel_one
eval_modulus_sub 📖	mathematical	—	DFunLike.coe DirichletCharacter ZMod MulChar.instFunLike CommRing.toCommMonoid ZMod.commRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	CharP.cast_eq_zero ZMod.charP zero_sub
even_or_odd 📖	mathematical	—	Even Odd	—	map_pow MulCharClass.toMonoidHomClass MulChar.instMulCharClass neg_one_sq map_one MonoidHomClass.toOneHomClass sq_eq_one_iff
factorsThrough_conductor 📖	mathematical	—	FactorsThrough conductor	—	conductor_mem_conductorSet
factorsThrough_gcd 📖	mathematical	DFunLike.coe MonoidHom DirichletCharacter MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup MulChar.commGroup ZMod CommRing.toCommMonoid ZMod.commRing MonoidHom.instFunLike changeLevel	FactorsThrough	—	factorsThrough_iff_ker_unitsMap MonoidHom.mem_ker Units.ext_iff MulChar.coe_toUnitHom Units.val_one ZMod.natCast_eq_natCast_iff Nat.cast_one ZMod.natCast_val ZMod.unitsMap_val ZMod.cast_id' ZMod.isUnit_iff_coprime Units.isUnit isUnit_one changeLevel_eq_cast_of_dvd ZMod.cast_natCast ZMod.charP map_one MonoidHomClass.toOneHomClass MulCharClass.toMonoidHomClass MulChar.instMulCharClass
factorsThrough_iff_ker_unitsMap 📖	mathematical	—	FactorsThrough Subgroup Units ZMod MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing Units.instGroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder MonoidHom.ker Units.instMulOneClass ZMod.unitsMap CommMonoid.toMonoid CommRing.toCommMonoid CommMonoidWithZero.toMonoidWithZero MulChar.toUnitHom	—	MonoidHom.mem_ker changeLevel_toUnitHom MonoidHom.comp_apply map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass ZMod.unitsMap_surjective MonoidHom.liftOfRightInverse_comp Equiv.injective Equiv.apply_symm_apply
factorsThrough_one_iff 📖	mathematical	—	FactorsThrough DirichletCharacter MulChar.hasOne ZMod CommRing.toCommMonoid ZMod.commRing	—	changeLevel_one level_one one_dvd
instSubsingletonOfNatNat 📖	mathematical	—	DirichletCharacter	—	subsingleton_iff level_one
isPrimitive_def 📖	mathematical	—	IsPrimitive conductor	—	—
isPrimitive_one_level_one 📖	mathematical	—	IsPrimitive DirichletCharacter MulChar.hasOne ZMod CommRing.toCommMonoid ZMod.commRing	—	conductor_dvd_level
isPrimitive_one_level_zero 📖	mathematical	—	IsPrimitive DirichletCharacter MulChar.hasOne ZMod CommRing.toCommMonoid ZMod.commRing	—	conductor_eq_zero_iff_level_eq_zero
level_mem_conductorSet 📖	mathematical	—	Set Set.instMembership conductorSet	—	FactorsThrough.same_level
level_one 📖	mathematical	—	DirichletCharacter MulChar.hasOne ZMod CommRing.toCommMonoid ZMod.commRing	—	MulChar.ext Units.eq_one Unique.instSubsingleton map_one MonoidHomClass.toOneHomClass MulCharClass.toMonoidHomClass MulChar.instMulCharClass
level_one' 📖	mathematical	—	DirichletCharacter MulChar.hasOne ZMod CommRing.toCommMonoid ZMod.commRing	—	level_one
map_zero' 📖	mathematical	—	DFunLike.coe DirichletCharacter ZMod MulChar.instFunLike CommRing.toCommMonoid ZMod.commRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero	—	ZMod.nontrivial_iff MulChar.map_zero
mem_conductorSet_dvd 📖	—	Set Set.instMembership conductorSet	—	—	FactorsThrough.dvd
mem_conductorSet_iff 📖	mathematical	—	Set Set.instMembership conductorSet FactorsThrough	—	—
mul_def 📖	mathematical	—	primitive_mul primitiveCharacter mul	—	—
not_even_and_odd 📖	mathematical	—	Even Odd	—	Nat.instAtLeastTwoHAddOfNat one_add_one_eq_two
primitiveCharacter_isPrimitive 📖	mathematical	—	IsPrimitive conductor primitiveCharacter	—	isPrimitive_def conductor_eq_zero_iff_level_eq_zero le_antisymm conductor_dvd_level conductor_le_conductor_mem_conductorSet conductor_mem_conductorSet
primitiveCharacter_one 📖	mathematical	—	primitiveCharacter DirichletCharacter MulChar.hasOne ZMod CommRing.toCommMonoid ZMod.commRing conductor	—	eq_one_iff_conductor_eq_one conductor_one isPrimitive_def primitiveCharacter_isPrimitive
primitive_mul_isPrimitive 📖	mathematical	—	IsPrimitive conductor mul primitive_mul	—	primitiveCharacter_isPrimitive
toUnitHom_eq_char' 📖	mathematical	IsUnit ZMod MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing	DFunLike.coe DirichletCharacter MulChar.instFunLike CommRing.toCommMonoid Units.val CommMonoidWithZero.toMonoidWithZero MonoidHom Units CommMonoid.toMonoid MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike MulChar.toUnitHom IsUnit.unit	—	MulChar.coe_equivToUnitHom
toUnitHom_inj 📖	mathematical	—	MulChar.toUnitHom ZMod CommRing.toCommMonoid ZMod.commRing	—	EquivLike.toEmbeddingLike
zero_ne_mem_conductorSet 📖	mathematical	—	Set Set.instMembership conductorSet	—	FactorsThrough.dvd

DirichletCharacter.Even

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eval_neg 📖	mathematical	DirichletCharacter.Even	DFunLike.coe DirichletCharacter CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring ZMod MulChar.instFunLike CommRing.toCommMonoid ZMod.commRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing	—	neg_one_mul map_mul MonoidHomClass.toMulHomClass MulCharClass.toMonoidHomClass MulChar.instMulCharClass eq_1 one_mul
not_odd 📖	mathematical	DirichletCharacter.Even	DirichletCharacter.Odd	—	Nat.instAtLeastTwoHAddOfNat DirichletCharacter.not_even_and_odd
toUnitHom_eval_neg_one 📖	mathematical	DirichletCharacter.Even	DFunLike.coe MonoidHom Units ZMod CommMonoid.toMonoid CommRing.toCommMonoid ZMod.commRing MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike MulChar.toUnitHom Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Units.instOne	—	MulChar.coe_toUnitHom
to_fun 📖	mathematical	DirichletCharacter.Even	Function.Even ZMod NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing ZMod.commRing DFunLike.coe DirichletCharacter CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring MulChar.instFunLike CommRing.toCommMonoid	—	neg_one_mul map_mul MonoidHomClass.toMulHomClass MulCharClass.toMonoidHomClass MulChar.instMulCharClass one_mul

DirichletCharacter.FactorsThrough

Definitions

Name	Category	Theorems
χ₀ 📖	CompOp	1 math math: eq_changeLevel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dvd 📖	—	DirichletCharacter.FactorsThrough	—	—	—
eq_changeLevel 📖	mathematical	DirichletCharacter.FactorsThrough	DFunLike.coe MonoidHom DirichletCharacter MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup MulChar.commGroup ZMod CommRing.toCommMonoid ZMod.commRing MonoidHom.instFunLike DirichletCharacter.changeLevel dvd χ₀	—	—
existsUnique 📖	mathematical	DirichletCharacter.FactorsThrough	ExistsUnique DirichletCharacter DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup MulChar.commGroup ZMod CommRing.toCommMonoid ZMod.commRing MonoidHom.instFunLike DirichletCharacter.changeLevel dvd	—	dvd DirichletCharacter.changeLevel_injective
same_level 📖	mathematical	—	DirichletCharacter.FactorsThrough	—	dvd_refl DirichletCharacter.changeLevel_self

DirichletCharacter.Odd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eval_neg 📖	mathematical	DirichletCharacter.Odd	DFunLike.coe DirichletCharacter CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring ZMod MulChar.instFunLike CommRing.toCommMonoid ZMod.commRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing	—	neg_one_mul map_mul MonoidHomClass.toMulHomClass MulCharClass.toMonoidHomClass MulChar.instMulCharClass eq_1 neg_mul one_mul
not_even 📖	mathematical	DirichletCharacter.Odd	DirichletCharacter.Even	—	Nat.instAtLeastTwoHAddOfNat DirichletCharacter.not_even_and_odd
toUnitHom_eval_neg_one 📖	mathematical	DirichletCharacter.Odd	DFunLike.coe MonoidHom Units ZMod CommMonoid.toMonoid CommRing.toCommMonoid ZMod.commRing MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike MulChar.toUnitHom Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Units.instOne	—	MulChar.coe_toUnitHom
to_fun 📖	mathematical	DirichletCharacter.Odd	Function.Odd ZMod NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing ZMod.commRing DFunLike.coe DirichletCharacter CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring MulChar.instFunLike CommRing.toCommMonoid	—	neg_one_mul map_mul MonoidHomClass.toMulHomClass MulCharClass.toMonoidHomClass MulChar.instMulCharClass

(root)

Definitions

Name	Category	Theorems
DirichletCharacter 📖	CompOp	76 math math: ArithmeticFunction.vonMangoldt.residueClass_eq, DirichletCharacter.changeLevel_injective, DirichletCharacter.Odd.eval_neg, DirichletCharacter.LSeries_eulerProduct_tprod, DirichletCharacter.LSeries_modOne_eq, DirichletCharacter.changeLevel_def, DirichletCharacter.LSeriesSummable_of_one_lt_re, DirichletCharacter.conductor_le_conductor_mem_conductorSet, DirichletCharacter.changeLevel_trans, DirichletCharacter.LSeries_twist_vonMangoldt_eq, DirichletCharacter.LFunction_eq_LSeries, DirichletCharacter.norm_LSeries_product_ge_one, DirichletCharacter.deriv_LFunction_eq_deriv_LSeries, DirichletCharacter.LFunction_changeLevel, DirichletCharacter.IsPrimitive.completedLFunction_one_sub, DirichletCharacter.primitiveCharacter_one, DirichletCharacter.norm_le_one, DirichletCharacter.mul_delta, DirichletCharacter.eval_modulus_sub, DirichletCharacter.instSubsingletonOfNatNat, DirichletCharacter.unit_norm_eq_one, DirichletCharacter.Odd.to_fun, DirichletCharacter.sum_characters_eq, ArithmeticFunction.vonMangoldt.residueClass_apply, DirichletCharacter.level_one', DirichletCharacter.LSeriesSummable_mul, DirichletCharacter.conductor_one, DirichletCharacter.LSeries_changeLevel, DirichletCharacter.mulEquiv_units, DirichletCharacter.changeLevel_one, DirichletCharacter.toUnitHom_eq_char', DirichletCharacter.changeLevel_toUnitHom, DirichletCharacter.level_one, DirichletCharacter.LSeries.mul_mu_eq_one, DirichletCharacter.sum_char_inv_mul_char_eq, gaussSum_aux_of_mulShift, DirichletCharacter.summable_neg_log_one_sub_mul_prime_cpow, gaussSum_mulShift_of_isPrimitive, DirichletCharacter.isPrimitive_one_level_one, DirichletCharacter.LSeriesSummable_twist_vonMangoldt, DirichletCharacter.isPrimitive_one_level_zero, DirichletCharacter.modOne_eq_one, DirichletCharacter.convolution_twist_vonMangoldt, DirichletCharacter.LSeriesSummable_iff, DirichletCharacter.IsPrimitive.fourierTransform_eq_inv_mul_gaussSum, DirichletCharacter.changeLevel_factorsThrough, DirichletCharacter.absicssaOfAbsConv_eq_one, DirichletCharacter.eq_one_iff_conductor_eq_one, DirichletCharacter.sum_characters_eq_zero, DirichletCharacter.mul_convolution_distrib, DirichletCharacter.norm_LFunction_product_ge_one, DirichletCharacter.LSeries_eulerProduct_hasProd, tsum_dirichletSummand, DirichletCharacter.LSeries_eulerProduct_exp_log, ArithmeticFunction.vonMangoldt.LSeries_residueClass_eq, DirichletCharacter.changeLevel_eq_one_iff, DirichletCharacter.FactorsThrough.existsUnique, DirichletCharacter.apply_eq_toArithmeticFunction_apply, DirichletCharacter.not_LSeriesSummable_at_one, DirichletCharacter.changeLevel_self_toUnitHom, DirichletCharacter.card_eq_totient_of_hasEnoughRootsOfUnity, DirichletCharacter.delta_mul, DirichletCharacter.isMultiplicative_toArithmeticFunction, DirichletCharacter.convolution_mul_moebius, DirichletCharacter.factorsThrough_one_iff, DirichletCharacter.Even.to_fun, DirichletCharacter.changeLevel_primitiveCharacter, DirichletCharacter.map_zero', DirichletCharacter.modZero_eq_delta, DirichletCharacter.fourierTransform_eq_gaussSum_mulShift, DirichletCharacter.LSeries_eulerProduct, DirichletCharacter.changeLevel_self, DirichletCharacter.conductor_one_dvd, DirichletCharacter.changeLevel_eq_cast_of_dvd, DirichletCharacter.FactorsThrough.eq_changeLevel, DirichletCharacter.Even.eval_neg

---

← Back to Index