Documentation Verification Report

Linearity

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

Statistics

Metric	Count
Definitions	0
Theorems `term_add`, `term_add_apply`, `term_neg`, `term_neg_apply`, `term_smul`, `term_smul_apply`, `term_sub`, `term_sub_apply`, `term_sum`, `term_sum_apply`, `add`, `neg`, `smul`, `sub`, `sum`, `add`, `neg`, `neg_iff`, `of_smul`, `smul`, `smul_iff`, `sub`, `sum`, `LSeries_add`, `LSeries_neg`, `LSeries_smul`, `LSeries_sub`, `LSeries_sum`	28
Total	28

LSeries

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`term_add` 📖	mathematical	—	`term` `Pi.instAdd` `Complex` `Complex.instAdd`	—	`add_zero` `term_of_ne_zero` `Nat.cast_add` `Nat.cast_one` `add_div`
`term_add_apply` 📖	mathematical	—	`term` `Pi.instAdd` `Complex` `Complex.instAdd`	—	`term_add`
`term_neg` 📖	mathematical	—	`term` `Pi.instNeg` `Complex` `Complex.instNeg`	—	`neg_zero` `term_of_ne_zero` `Nat.cast_add` `Nat.cast_one` `neg_div`
`term_neg_apply` 📖	mathematical	—	`term` `Pi.instNeg` `Complex` `Complex.instNeg`	—	`term_neg`
`term_smul` 📖	mathematical	—	`term` `Complex` `Function.hasSMul` `Algebra.toSMul` `Complex.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	—	`MulZeroClass.mul_zero` `term_of_ne_zero` `Nat.cast_add` `Nat.cast_one` `mul_div_assoc`
`term_smul_apply` 📖	mathematical	—	`term` `Complex` `Function.hasSMul` `Algebra.toSMul` `Complex.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Complex.instMul`	—	`term_smul`
`term_sub` 📖	mathematical	—	`term` `Pi.instSub` `Complex` `Complex.instSub`	—	`sub_eq_add_neg` `term_add` `term_neg`
`term_sub_apply` 📖	mathematical	—	`term` `Pi.instSub` `Complex` `Complex.instSub`	—	`term_sub` `Pi.sub_apply`
`term_sum` 📖	mathematical	—	`term` `Finset.sum` `Pi.addCommMonoid` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup`	—	`term_sum_apply` `Finset.sum_apply`
`term_sum_apply` 📖	mathematical	—	`term` `Finset.sum` `Pi.addCommMonoid` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup`	—	`eq_or_ne` `Finset.sum_congr` `Finset.sum_const_zero` `term_of_ne_zero` `Finset.sum_apply` `Finset.sum_div`

LSeriesHasSum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`LSeriesHasSum`	`LSeriesHasSum` `Pi.instAdd` `Complex` `Complex.instAdd`	—	`LSeries.term_add` `HasSum.add` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing`
`neg` 📖	mathematical	`LSeriesHasSum`	`LSeriesHasSum` `Pi.instNeg` `Complex` `Complex.instNeg`	—	`LSeries.term_neg` `HasSum.neg` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`smul` 📖	mathematical	`LSeriesHasSum`	`LSeriesHasSum` `Complex` `Function.hasSMul` `Algebra.toSMul` `Complex.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Complex.instMul`	—	`LSeries.term_smul` `HasSum.const_smul` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing`
`sub` 📖	mathematical	`LSeriesHasSum`	`LSeriesHasSum` `Pi.instSub` `Complex` `Complex.instSub`	—	`LSeries.term_sub` `HasSum.sub` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`sum` 📖	mathematical	`LSeriesHasSum`	`LSeriesHasSum` `Finset.sum` `Pi.addCommMonoid` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup`	—	`LSeries.term_sum` `Finset.sum_fn` `hasSum_sum` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing`

LSeriesSummable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`LSeriesSummable`	`LSeriesSummable` `Pi.instAdd` `Complex` `Complex.instAdd`	—	`Summable.add` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing`
`neg` 📖	mathematical	`LSeriesSummable`	`LSeriesSummable` `Pi.instNeg` `Complex` `Complex.instNeg`	—	`LSeries.term_neg` `Summable.neg` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`neg_iff` 📖	mathematical	—	`LSeriesSummable` `Pi.instNeg` `Complex` `Complex.instNeg`	—	`neg` `neg_neg`
`of_smul` 📖	mathematical	`LSeriesSummable` `Complex` `Function.hasSMul` `Algebra.toSMul` `Complex.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	`LSeriesSummable`	—	`inv_smul_smul₀` `smul`
`smul` 📖	mathematical	`LSeriesSummable`	`LSeriesSummable` `Complex` `Function.hasSMul` `Algebra.toSMul` `Complex.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	—	`LSeries.term_smul` `Summable.const_smul` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing`
`smul_iff` 📖	mathematical	—	`LSeriesSummable` `Complex` `Function.hasSMul` `Algebra.toSMul` `Complex.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	—	`of_smul` `smul`
`sub` 📖	mathematical	`LSeriesSummable`	`LSeriesSummable` `Pi.instSub` `Complex` `Complex.instSub`	—	`Summable.sub` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`sum` 📖	mathematical	`LSeriesSummable`	`LSeriesSummable` `Finset.sum` `Pi.addCommMonoid` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup`	—	`summable_sum` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`LSeries_add` 📖	mathematical	`LSeriesSummable`	`LSeries` `Pi.instAdd` `Complex` `Complex.instAdd`	—	`LSeries.term_add` `Summable.tsum_add` `Complex.instT2Space` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SummationFilter.instNeBotUnconditional`
`LSeries_neg` 📖	mathematical	—	`LSeries` `Pi.instNeg` `Complex` `Complex.instNeg`	—	`LSeries.term_neg_apply` `tsum_neg` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Complex.instT2Space`
`LSeries_smul` 📖	mathematical	—	`LSeries` `Complex` `Function.hasSMul` `Algebra.toSMul` `Complex.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Complex.instMul`	—	`LSeries.term_smul_apply` `tsum_mul_left` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Complex.instT2Space`
`LSeries_sub` 📖	mathematical	`LSeriesSummable`	`LSeries` `Pi.instSub` `Complex` `Complex.instSub`	—	`LSeries.term_sub` `Summable.tsum_sub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Complex.instT2Space` `SummationFilter.instNeBotUnconditional`
`LSeries_sum` 📖	mathematical	`LSeriesSummable`	`LSeries` `Finset.sum` `Pi.addCommMonoid` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup`	—	`LSeries.term_sum_apply` `Finset.sum_congr` `Summable.tsum_finsetSum` `Complex.instT2Space` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SummationFilter.instNeBotUnconditional`

---

← Back to Index