Documentation Verification Report

DirichletContinuation

📁 Source: Mathlib/NumberTheory/LSeries/DirichletContinuation.lean

Statistics

Metric	Count
Definitions `LFunctionTrivChar`, `LFunctionTrivChar₁`, `completedLFunction`, `gammaFactor`, `rootNumber`	5
Theorems `LFunction_neg_two_mul_nat`, `LFunction_neg_two_mul_nat_add_one`, `gammaFactor_def`, `completedLFunction_one_sub`, `LFunctionTrivChar_eq_mul_riemannZeta`, `LFunctionTrivChar_residue_one`, `LFunctionTrivChar₁_apply_one_ne_zero`, `LFunction_changeLevel`, `LFunction_eq_LSeries`, `LFunction_eq_completed_div_gammaFactor`, `LFunction_modOne_eq`, `LFunction_neg_two_mul_nat_sub_one`, `gammaFactor_def`, `completedLFunction_modOne_eq`, `continuousOn_neg_logDeriv_LFunctionTrivChar₁`, `continuousOn_neg_logDeriv_LFunction_of_nontriv`, `deriv_LFunctionTrivChar₁_apply_of_ne_one`, `deriv_LFunction_eq_deriv_LSeries`, `differentiableAt_LFunction`, `differentiableAt_completedLFunction`, `differentiable_LFunction`, `differentiable_LFunctionTrivChar₁`, `differentiable_completedLFunction`, `rootNumber_modOne`	24
Total	29

DirichletCharacter

Definitions

Name	Category	Theorems
`LFunctionTrivChar` 📖	CompOp	6 math math: `LFunctionTrivChar_eq_mul_riemannZeta`, `deriv_LFunctionTrivChar₁_apply_of_ne_one`, `norm_LFunction_product_ge_one`, `LFunctionTrivChar_isBigO_near_one_horizontal`, `LFunctionTrivChar_residue_one`, `continuousOn_neg_logDeriv_LFunctionTrivChar₁`
`LFunctionTrivChar₁` 📖	CompOp	3 math math: `deriv_LFunctionTrivChar₁_apply_of_ne_one`, `differentiable_LFunctionTrivChar₁`, `continuousOn_neg_logDeriv_LFunctionTrivChar₁`
`completedLFunction` 📖	CompOp	5 math math: `IsPrimitive.completedLFunction_one_sub`, `LFunction_eq_completed_div_gammaFactor`, `differentiableAt_completedLFunction`, `completedLFunction_modOne_eq`, `differentiable_completedLFunction`
`gammaFactor` 📖	CompOp	3 math math: `LFunction_eq_completed_div_gammaFactor`, `Even.gammaFactor_def`, `Odd.gammaFactor_def`
`rootNumber` 📖	CompOp	2 math math: `IsPrimitive.completedLFunction_one_sub`, `rootNumber_modOne`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`LFunctionTrivChar_eq_mul_riemannZeta` 📖	mathematical	—	`LFunctionTrivChar` `Complex` `Complex.instMul` `Finset.prod` `CommRing.toCommMonoid` `Complex.commRing` `Nat.primeFactors` `Complex.instSub` `Complex.instOne` `Complex.instPow` `Complex.instNatCast` `Complex.instNeg` `riemannZeta`	—	`LFunction_modOne_eq` `LFunctionTrivChar.eq_1` `changeLevel_one` `mul_comm` `Finset.prod_congr` `MulChar.one_apply` `isUnit_of_subsingleton` `Unique.instSubsingleton` `one_mul` `LFunction_changeLevel`
`LFunctionTrivChar_residue_one` 📖	mathematical	—	`Filter.Tendsto` `Complex` `Complex.instMul` `Complex.instSub` `Complex.instOne` `LFunctionTrivChar` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `nhds` `Finset.prod` `CommRing.toCommMonoid` `Complex.commRing` `Nat.primeFactors` `Complex.instInv` `Complex.instNatCast`	—	`Set.EqOn.eventuallyEq_nhdsWithin` `mul_left_comm` `LFunctionTrivChar_eq_mul_riemannZeta` `Filter.tendsto_congr'` `mul_one` `Complex.cpow_neg_one` `Filter.Tendsto.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `tendsto_nhdsWithin_of_tendsto_nhds` `Continuous.tendsto` `continuous_finset_prod` `Nat.Prime.ne_zero` `Nat.prime_of_mem_primeFactors` `Continuous.sub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `continuous_const` `Continuous.comp'` `continuous_const_cpow` `NeZero.charZero` `Complex.instCharZero` `Continuous.neg` `IsSemitopologicalRing.toContinuousNeg` `IsTopologicalRing.toIsSemitopologicalRing` `continuous_id'` `riemannZeta_residue_one`
`LFunctionTrivChar₁_apply_one_ne_zero` 📖	—	—	—	—	`Function.update_self` `Finset.prod_ne_zero_iff` `Complex.instNontrivial` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Complex.instCharZero` `Nat.Prime.ne_one` `Nat.prime_of_mem_primeFactors`
`LFunction_changeLevel` 📖	mathematical	—	`LFunction` `DFunLike.coe` `MonoidHom` `DirichletCharacter` `Complex` `CommGroupWithZero.toCommMonoidWithZero` `Semifield.toCommGroupWithZero` `Field.toSemifield` `Complex.instField` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `MulChar.commGroup` `ZMod` `CommRing.toCommMonoid` `ZMod.commRing` `MonoidHom.instFunLike` `changeLevel` `Complex.instMul` `Finset.prod` `Complex.commRing` `Nat.primeFactors` `Complex.instSub` `Complex.instOne` `MulChar.instFunLike` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Complex.instPow` `Complex.instNatCast` `Complex.instNeg`	—	`changeLevel_eq_one_iff` `Continuous.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Differentiable.continuous` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `differentiable_LFunction` `continuous_finset_prod` `Nat.Prime.ne_zero` `Nat.prime_of_mem_primeFactors` `Continuous.sub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `continuous_const` `Continuous.const_mul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `Continuous.comp'` `continuous_const_cpow` `NeZero.charZero` `Complex.instCharZero` `Continuous.neg` `IsSemitopologicalRing.toContinuousNeg` `continuous_id'` `Continuous.ext_on` `Complex.instT2Space` `dense_compl_singleton` `PerfectSpace.not_isolated` `instPerfectSpace`
`LFunction_eq_LSeries` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Complex.re`	`LFunction` `LSeries` `DFunLike.coe` `DirichletCharacter` `Complex` `CommGroupWithZero.toCommMonoidWithZero` `Semifield.toCommGroupWithZero` `Field.toSemifield` `Complex.instField` `ZMod` `MulChar.instFunLike` `CommRing.toCommMonoid` `ZMod.commRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`ZMod.LFunction_eq_LSeries`
`LFunction_eq_completed_div_gammaFactor` 📖	mathematical	—	`LFunction` `Complex` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `completedLFunction` `gammaFactor`	—	`even_or_odd` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Even.gammaFactor_def` `ZMod.LFunction_eq_completed_div_gammaFactor_even` `Even.to_fun` `map_zero'` `Odd.gammaFactor_def` `ZMod.LFunction_eq_completed_div_gammaFactor_odd` `Odd.to_fun`
`LFunction_modOne_eq` 📖	mathematical	—	`LFunction` `riemannZeta`	—	`LFunction.eq_1` `ZMod.LFunction_modOne_eq` `map_one` `MonoidHomClass.toOneHomClass` `MulCharClass.toMonoidHomClass` `MulChar.instMulCharClass` `one_mul`
`completedLFunction_modOne_eq` 📖	mathematical	—	`completedLFunction` `completedRiemannZeta`	—	`completedLFunction.eq_1` `ZMod.completedLFunction_modOne_eq` `map_one` `MonoidHomClass.toOneHomClass` `MulCharClass.toMonoidHomClass` `MulChar.instMulCharClass` `one_mul`
`continuousOn_neg_logDeriv_LFunctionTrivChar₁` 📖	mathematical	—	`ContinuousOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instNeg` `deriv` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `LFunctionTrivChar₁` `setOf` `Complex.instOne` `LFunctionTrivChar` `Complex.instZero`	—	`neg_div` `differentiable_LFunctionTrivChar₁` `ContinuousOn.neg` `IsSemitopologicalRing.toContinuousNeg` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousOn.div` `IsTopologicalDivisionRing.toContinuousInv₀` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `Continuous.continuousOn` `ContDiff.continuous_deriv` `Differentiable.contDiff` `Complex.instCompleteSpace` `le_rfl` `Differentiable.continuous` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `eq_or_ne` `LFunctionTrivChar₁_apply_one_ne_zero` `LFunctionTrivChar₁.eq_1` `Function.update_of_ne` `mul_ne_zero_iff` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `sub_ne_zero_of_ne` `Set.mem_setOf`
`continuousOn_neg_logDeriv_LFunction_of_nontriv` 📖	mathematical	—	`ContinuousOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instNeg` `deriv` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `LFunction` `setOf` `Complex.instZero`	—	`differentiable_LFunction` `neg_div` `ContinuousOn.neg` `IsSemitopologicalRing.toContinuousNeg` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousOn.div` `IsTopologicalDivisionRing.toContinuousInv₀` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `Continuous.continuousOn` `ContDiff.continuous_deriv` `Differentiable.contDiff` `Complex.instCompleteSpace` `le_rfl` `Differentiable.continuous` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology`
`deriv_LFunctionTrivChar₁_apply_of_ne_one` 📖	mathematical	—	`deriv` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `LFunctionTrivChar₁` `Complex.instAdd` `Complex.instMul` `Complex.instSub` `Complex.instOne` `LFunctionTrivChar`	—	`Filter.EventuallyEq.deriv_eq` `Filter.eventuallyEq_iff_exists_mem` `IsOpen.mem_nhds` `isOpen_ne` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `Function.update_of_ne` `Set.mem_setOf` `deriv_fun_mul` `DifferentiableAt.sub_const` `differentiableAt_id` `differentiableAt_LFunction` `deriv_sub_const` `deriv_id''` `one_mul` `add_comm`
`deriv_LFunction_eq_deriv_LSeries` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Complex.re`	`deriv` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `LFunction` `LSeries` `DFunLike.coe` `DirichletCharacter` `CommGroupWithZero.toCommMonoidWithZero` `Semifield.toCommGroupWithZero` `Field.toSemifield` `Complex.instField` `ZMod` `MulChar.instFunLike` `CommRing.toCommMonoid` `ZMod.commRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`Filter.EventuallyEq.deriv_eq` `IsOpen.mem_nhds` `isOpen_lt` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `continuous_const` `Complex.continuous_re` `Filter.mp_mem` `Filter.univ_mem'` `LFunction_eq_LSeries`
`differentiableAt_LFunction` 📖	mathematical	—	`DifferentiableAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `LFunction`	—	`ZMod.differentiableAt_LFunction` `MulChar.sum_eq_zero_of_ne_one` `instIsDomain`
`differentiableAt_completedLFunction` 📖	mathematical	—	`DifferentiableAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `completedLFunction`	—	`ZMod.differentiableAt_completedLFunction` `map_zero'` `MulChar.sum_eq_zero_of_ne_one` `instIsDomain`
`differentiable_LFunction` 📖	mathematical	—	`Differentiable` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `LFunction`	—	`differentiableAt_LFunction`
`differentiable_LFunctionTrivChar₁` 📖	mathematical	—	`Differentiable` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `LFunctionTrivChar₁`	—	`differentiableOn_univ` `Complex.differentiableOn_compl_singleton_and_continuousAt_iff` `Complex.instCompleteSpace` `Filter.univ_mem` `DifferentiableOn.congr` `DifferentiableAt.differentiableWithinAt` `DifferentiableAt.fun_mul` `DifferentiableAt.sub_const` `differentiableAt_id` `differentiableAt_LFunction` `Function.update_of_ne` `Set.mem_diff_singleton` `continuousWithinAt_compl_self` `LFunctionTrivChar_residue_one`
`differentiable_completedLFunction` 📖	mathematical	—	`Differentiable` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `completedLFunction`	—	`differentiableAt_completedLFunction` `level_one'`
`rootNumber_modOne` 📖	mathematical	—	`rootNumber` `Complex` `Complex.instOne`	—	`Finset.sum_congr` `Finset.singleton_eq_univ` `Unique.instSubsingleton` `Finset.sum_singleton` `map_one` `MonoidHomClass.toOneHomClass` `MulCharClass.toMonoidHomClass` `MulChar.instMulCharClass` `AddChar.map_zero_eq_one` `mul_one` `pow_zero` `div_self` `NeZero.charZero_one` `Complex.instCharZero` `Nat.cast_one` `one_div` `Complex.one_cpow`

DirichletCharacter.Even

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`LFunction_neg_two_mul_nat` 📖	mathematical	`DirichletCharacter.Even` `Complex` `Complex.commRing`	`DirichletCharacter.LFunction` `Complex` `Complex.instNeg` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.instZero`	—	`Nat.instAtLeastTwoHAddOfNat` `DirichletCharacter.LFunction.congr_simp` `Nat.cast_one` `Nat.cast_zero` `LFunction_neg_two_mul_nat_add_one`
`LFunction_neg_two_mul_nat_add_one` 📖	mathematical	`DirichletCharacter.Even` `Complex` `Complex.commRing`	`DirichletCharacter.LFunction` `Complex` `Complex.instNeg` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.instAdd` `Complex.instOne` `Complex.instZero`	—	`ZMod.LFunction_neg_two_mul_nat_add_one` `to_fun`
`gammaFactor_def` 📖	mathematical	`DirichletCharacter.Even` `Complex` `Complex.commRing`	`DirichletCharacter.gammaFactor` `Complex.Gammaℝ`	—	—

DirichletCharacter.IsPrimitive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`completedLFunction_one_sub` 📖	mathematical	`DirichletCharacter.IsPrimitive` `Complex` `CommGroupWithZero.toCommMonoidWithZero` `Semifield.toCommGroupWithZero` `Field.toSemifield` `Complex.instField`	`DirichletCharacter.completedLFunction` `Complex` `Complex.instSub` `Complex.instOne` `Complex.instMul` `Complex.instPow` `Complex.instNatCast` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat` `DirichletCharacter.rootNumber` `DirichletCharacter` `CommGroupWithZero.toCommMonoidWithZero` `Semifield.toCommGroupWithZero` `Field.toSemifield` `Complex.instField` `MulChar.hasInv` `ZMod` `CommRing.toCommMonoid` `ZMod.commRing`	—	`Nat.instAtLeastTwoHAddOfNat` `eq_or_ne` `DirichletCharacter.completedLFunction_modOne_eq` `completedRiemannZeta_one_sub` `Nat.cast_one` `one_div` `Complex.one_cpow` `DirichletCharacter.rootNumber_modOne` `mul_one` `one_mul` `MulChar.sum_eq_zero_of_ne_one` `instIsDomain` `DirichletCharacter.conductor_one` `eq_1` `DirichletCharacter.rootNumber.eq_1` `mul_comm_div` `Complex.cpow_sub` `NeZero.charZero` `Complex.instCharZero` `sub_sub` `add_halves` `CharZero.NeZero.two` `RingHomInvPair.ids` `pow_zero` `div_one` `DirichletCharacter.completedLFunction.eq_1` `ZMod.completedLFunction_one_sub_even` `DirichletCharacter.Even.to_fun` `DirichletCharacter.map_zero'` `DirichletCharacter.even_or_odd` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `ZMod.completedLFunction_one_sub_odd` `DirichletCharacter.Odd.to_fun` `pow_one` `Complex.div_I` `mul_neg_one` `neg_mul` `neg_neg` `fourierTransform_eq_inv_mul_gaussSum` `neg_one_mul` `map_mul` `MonoidHomClass.toMulHomClass` `MulCharClass.toMonoidHomClass` `MulChar.instMulCharClass` `mul_right_comm` `ZMod.completedLFunction_const_mul` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `MulChar.mul_apply` `mul_inv_cancel` `MulChar.one_apply` `IsUnit.neg` `isUnit_one`

DirichletCharacter.Odd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`LFunction_neg_two_mul_nat_sub_one` 📖	mathematical	`DirichletCharacter.Odd` `Complex` `Complex.commRing`	`DirichletCharacter.LFunction` `Complex` `Complex.instSub` `Complex.instNeg` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.instOne` `Complex.instZero`	—	`ZMod.LFunction_neg_two_mul_nat_sub_one` `to_fun`
`gammaFactor_def` 📖	mathematical	`DirichletCharacter.Odd` `Complex` `Complex.commRing`	`DirichletCharacter.gammaFactor` `Complex.Gammaℝ` `Complex` `Complex.instAdd` `Complex.instOne`	—	`not_even` `CharZero.NeZero.two` `Complex.instCharZero`

---

← Back to Index