Documentation Verification Report

BigOperators

📁 Source: Mathlib/Algebra/Order/CauSeq/BigOperators.lean

Statistics

Metric	Count
Definitions	0
Theorems `geo_series`, `geo_series_const`, `of_abv`, `of_abv_le`, `of_decreasing_bounded`, `of_mono_bounded`, `series_ratio_test`, `cauchy_product`	8
Total	8

IsCauSeq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`geo_series` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	`IsCauSeq` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	—	`of_abv` `congr_simp` `Finset.sum_congr` `IsAbsoluteValue.abv_pow` `IsStrictOrderedRing.isDomain` `AddGroup.existsAddOfLE` `geom_sum_eq` `neg_div_neg_eq` `neg_sub` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `of_mono_bounded` `abs_of_nonneg` `div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `sub_nonneg` `pow_le_one₀` `IsOrderedRing.toPosMulMono` `IsAbsoluteValue.abv_nonneg` `LT.lt.le` `le_of_lt` `div_le_div_of_nonneg_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `sub_le_self` `one_mul` `pow_succ'` `sub_le_sub_left` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass`
`geo_series_const` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `abs` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	`IsCauSeq` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Finset.range` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`congr_simp` `Finset.mul_sum` `mul` `IsAbsoluteValue.abs_isAbsoluteValue` `const` `geo_series` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero`
`of_abv` 📖	mathematical	`IsCauSeq` `DivisionRing.toRing` `Field.toDivisionRing` `abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Finset.range`	`NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`of_abv_le` `le_rfl`
`of_abv_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsCauSeq` `DivisionRing.toRing` `Field.toDivisionRing` `abs` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Finset.range`	`NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`Nat.instAtLeastTwoHAddOfNat` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toIsOrderedRing` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `le_trans` `le_max_right` `abs_sub_le` `IsOrderedRing.toIsOrderedAddMonoid` `add_lt_add` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `lt_of_le_of_lt` `tsub_eq_iff_eq_add_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `contravariant_lt_of_covariant_le` `Finset.sum_congr` `zero_add` `sub_self` `IsAbsoluteValue.abv_zero` `Finset.sum_range_succ_comm` `sub_eq_add_neg` `add_assoc` `le_imp_le_of_le_of_le` `IsAbsoluteValue.abv_add` `le_refl` `add_le_add_left` `add_le_add_right` `le_abs_self` `add_halves` `ZeroLEOneClass.neZero.two` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `abs_sub_comm`
`of_decreasing_bounded` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `abs` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	`IsCauSeq`	—	`Archimedean.arch` `lt_of_lt_of_le` `lt_neg` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `LE.le.trans_lt` `neg_sub` `lt_sub_iff_add_lt` `add_nsmul` `one_nsmul` `add_lt_add_of_le_of_lt` `lt_of_le_of_lt` `lt_add_of_pos_right` `neg_le` `le_abs_self` `abs_neg` `Nat.find_spec` `not_lt_of_ge` `le_rfl` `le_refl` `zero_nsmul` `sub_zero` `Nat.find_min` `GE.ge.le` `Nat.rel_of_forall_rel_succ_of_le_of_le` `instReflGe` `instIsTransGe` `not_lt` `abs_of_nonpos` `sub_nonpos` `sub_lt_iff_lt_add'` `succ_nsmul` `sub_add` `add_sub_cancel_right` `add_lt_add_left` `LE.le.trans`
`of_mono_bounded` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `abs` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	`IsCauSeq`	—	`of_neg` `IsAbsoluteValue.abs_isAbsoluteValue` `of_decreasing_bounded` `abs_neg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `covariant_swap_add_of_covariant_add`
`series_ratio_test` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Preorder.toLT` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`IsCauSeq` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finset.range`	—	`abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `of_abv_le` `LE.le.eq_or_lt` `lt_of_lt_of_le` `inv_zero` `pow_succ` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `tsub_eq_iff_eq_add_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `mul_right_comm` `inv_pow` `div_eq_mul_inv` `mul_div_cancel_right₀` `GroupWithZero.toMulDivCancelClass` `ne_of_gt` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toZeroLEOneClass` `le_refl` `zero_add` `add_le_add` `covariant_swap_add_of_covariant_add` `mul_assoc` `le_trans` `mul_comm` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `geo_series_const`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cauchy_product` 📖	mathematical	`IsCauSeq` `DivisionRing.toRing` `Field.toDivisionRing` `abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Finset.range` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`IsCauSeq.bounded` `IsAbsoluteValue.abs_isAbsoluteValue` `lt_of_le_of_lt` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `covariant_swap_add_of_covariant_add` `Nat.instAtLeastTwoHAddOfNat` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `mul_pos` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `IsCauSeq.cauchy₂` `IsAbsoluteValue.abv_nonneg` `Finset.sum_range_diag_flip` `Finset.mul_sum` `Finset.sum_add_distrib` `Finset.sum_congr` `mul_add` `Distrib.leftDistribClass` `sub_add_cancel` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.isNat_mul` `MulZeroClass.mul_zero` `div_zero` `mul_ne_zero` `IsStrictOrderedRing.noZeroDivisors` `AddGroup.existsAddOfLE` `two_ne_zero` `ZeroLEOneClass.neZero.two` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `div_div` `div_mul_cancel₀` `ne_of_lt` `mul_assoc` `add_halves` `lt_of_lt_of_le` `two_mul` `lt_add_of_pos_left` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instIsOrderedAddMonoid` `le_max_left` `Finset.sum_le_sum` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `le_of_lt` `le_tsub_of_add_le_left` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `LE.le.trans'` `add_le_add` `LT.lt.le` `Finset.mem_range` `abs_of_nonneg` `Finset.sum_nonneg` `Finset.sum_mul` `sub_sub` `sub_right_comm` `sub_self` `zero_sub` `IsAbsoluteValue.abv_neg` `IsAbsoluteValue.abv_sum` `add_lt_add_of_lt_of_lt` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `mul_comm` `mul_lt_mul_of_pos_left` `Mathlib.Meta.Positivity.pos_of_isNat` `Finset.sum_range_sub_sum_range` `sub_eq_add_neg` `le_imp_le_of_le_of_le` `IsAbsoluteValue.abv_add` `le_refl` `mul_lt_mul_of_pos_right` `IsStrictOrderedRing.toMulPosStrictMono` `LE.le.trans_lt` `le_abs_self` `LE.le.trans` `le_max_right` `IsAbsoluteValue.abv_mul` `add_sub_cancel`

---

← Back to Index