Documentation Verification Report

SumOverResidueClass

📁 Source: Mathlib/Analysis/SumOverResidueClass.lean

Statistics

Metric	Count
Definitions	0
Theorems `sum_indicator_mod`, `sumByResidueClasses`, `not_summable_indicator_mod_of_antitone_of_neg`, `not_summable_of_antitone_of_neg`, `summable_indicator_mod_iff`, `summable_indicator_mod_iff_summable`, `summable_indicator_mod_iff_summable_indicator_mod`	7
Total	7

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sum_indicator_mod` 📖	mathematical	—	`sum` `ZMod` `Pi.addCommMonoid` `univ` `ZMod.fintype` `Set.indicator` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `setOf` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `ZMod.commRing`	—	`sum_apply` `sum_congr` `Set.indicator_apply` `sum_ite_eq`

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sumByResidueClasses` 📖	mathematical	`Summable` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	`tsum` `Finset.sum` `ZMod` `Finset.univ` `ZMod.fintype` `ZMod.val`	—	`Equiv.tsum_eq` `Summable.tsum_prod` `Summable.comp_injective` `Equiv.injective` `tsum_fintype` `SummationFilter.instLeAtTopUnconditional` `residueClassesEquiv.eq_1`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`not_summable_indicator_mod_of_antitone_of_neg` 📖	mathematical	`Antitone` `Real` `Nat.instPreorder` `Real.instPreorder` `Real.instLT` `Real.instZero`	`Summable` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Set.indicator` `setOf` `ZMod` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `ZMod.commRing` `SummationFilter.unconditional`	—	`ZMod.natCast_zmod_val` `summable_indicator_mod_iff_summable` `instIsTopologicalAddGroupReal` `not_summable_of_antitone_of_neg` `Antitone.comp_monotone` `Monotone.add_const` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Covariant.monotone_of_const` `Nat.instMulLeftMono` `LE.le.trans_lt` `LE.le.trans`
`not_summable_of_antitone_of_neg` 📖	mathematical	`Antitone` `Real` `Nat.instPreorder` `Real.instPreorder` `Real.instLT` `Real.instZero`	`Summable` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SummationFilter.unconditional`	—	`Summable.tendsto_atTop_zero` `instIsTopologicalAddGroupReal` `dist_zero_right` `abs_pos_of_neg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Mathlib.Tactic.Contrapose.contrapose₁` `abs_of_neg` `LE.le.trans_lt` `neg_le_neg_iff` `covariant_swap_add_of_covariant_add`
`summable_indicator_mod_iff` 📖	mathematical	`Antitone` `Real` `Nat.instPreorder` `Real.instPreorder`	`Summable` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Set.indicator` `Real.instZero` `setOf` `ZMod` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `ZMod.commRing` `SummationFilter.unconditional`	—	`Finset.sum_indicator_mod` `Finset.sum_apply` `summable_sum` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `summable_indicator_mod_iff_summable_indicator_mod` `Summable.indicator` `instIsUniformAddGroupReal` `Real.instCompleteSpace`
`summable_indicator_mod_iff_summable` 📖	mathematical	—	`Summable` `AddCommGroup.toAddCommMonoid` `Set.indicator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `setOf` `ZMod` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `ZMod.commRing` `SummationFilter.unconditional`	—	`Set.Finite.summable_compl_iff` `Set.finite_lt_nat` `Set.indicator_indicator` `Set.inter_comm` `IsCancelMulZero.toIsLeftCancelMulZero` `Nat.instIsCancelMulZero` `Mathlib.Tactic.Contrapose.contrapose₂` `Set.mem_of_indicator_ne_zero` `Nat.range_mul_add` `Set.indicator_of_mem` `Nat.cast_add` `Nat.cast_mul` `CharP.cast_eq_zero` `ZMod.charP` `MulZeroClass.zero_mul` `zero_add` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd` `Function.Injective.summable_iff`
`summable_indicator_mod_iff_summable_indicator_mod` 📖	—	`Antitone` `Real` `Nat.instPreorder` `Real.instPreorder` `Summable` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Set.indicator` `Real.instZero` `setOf` `ZMod` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `ZMod.commRing` `SummationFilter.unconditional`	—	—	`ZMod.natCast_val` `ZMod.cast_id'` `CharP.cast_eq_zero` `ZMod.charP` `add_zero` `Nat.cast_add` `summable_indicator_mod_iff_summable` `instIsTopologicalAddGroupReal` `Summable.of_nonneg_of_le` `LT.lt.le` `LT.lt.trans_le` `ZMod.val_lt` `ZMod.natCast_zmod_val` `Mathlib.Tactic.Push.not_forall_eq` `not_summable_indicator_mod_of_antitone_of_neg`

---

← Back to Index