GeomSum

📁 Source: Mathlib/Algebra/Order/Field/GeomSum.lean

Statistics

Metric	Count
Definitions	0
Theorems geom_sum_Ico_le_of_lt_one, geom_sum_lt, geom_sum_of_lt_one, geom_sum_of_one_lt, geom₂_sum_of_gt, geom₂_sum_of_lt	6
Total	6

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
geom_sum_Ico_le_of_lt_one 📖	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	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.Ico Nat.instPreorder Nat.instLocallyFiniteOrder Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivInvMonoid.toDiv DivisionRing.toDivInvMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup	—	le_or_gt geom_sum_Ico' LT.lt.ne div_le_div₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono pow_nonneg IsStrictOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing AddGroup.toOrderedSub covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd le_rfl Finset.Ico_eq_empty LT.lt.le Finset.sum_empty div_nonneg
geom_sum_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Finset.range Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	—	geom_sum_of_lt_one div_lt_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono tsub_pos_iff_lt inv_mul_cancel₀ tsub_eq_zero_iff_le not_le tsub_lt_self_iff IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsStrictOrderedRing.toIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing LT.lt.trans pos_iff_ne_zero pow_pos IsStrictOrderedRing.toPosMulStrictMono IsStrictOrderedRing.toZeroLEOneClass
geom_sum_of_lt_one 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Finset.range Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero	—	eq_div_of_mul_eq LT.lt.ne' tsub_pos_of_lt geom_sum_mul_of_le_one IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsStrictOrderedRing.toIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE LT.lt.le
geom_sum_of_one_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Finset.range Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero	—	eq_div_of_mul_eq LT.lt.ne' tsub_pos_of_lt geom_sum_mul_of_one_le IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsStrictOrderedRing.toIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE LT.lt.le
geom₂_sum_of_gt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Finset.range Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero	—	eq_div_of_mul_eq LT.lt.ne' tsub_pos_of_lt geom_sum₂_mul_of_ge IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsStrictOrderedRing.toIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE LT.lt.le
geom₂_sum_of_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Finset.range Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero	—	eq_div_of_mul_eq LT.lt.ne' tsub_pos_of_lt geom_sum₂_mul_of_le IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsStrictOrderedRing.toIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE LT.lt.le

---

← Back to Index