GeomSum

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

Statistics

Metric	Count
Definitions	0
Theorems geomSum_lt, geom_sum_Ico_le, geom_sum_le, pred_mul_geom_sum_le, geom_sum_pos, geom_sum_alternating_of_le_neg_one, geom_sum_alternating_of_lt_neg_one, geom_sum_eq_zero_iff_neg_one, geom_sum_ne_zero, geom_sum_neg_iff, geom_sum_pos, geom_sum_pos', geom_sum_pos_and_lt_one, geom_sum_pos_iff	14
Total	14

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
geomSum_lt 📖	mathematical	—	Finset.sum instAddCommMonoid Monoid.toPow instMonoid	—	Finset.sum_le_sum_of_subset instCanonicallyOrderedAdd Finset.mem_range geomSum_eq tsub_lt_self instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid
geom_sum_Ico_le 📖	mathematical	—	Finset.sum instAddCommMonoid Finset.Ico instPreorder instLocallyFiniteOrder Monoid.toPow instMonoid	—	Finset.Ico_eq_empty_of_le Finset.sum_empty add_le_add_iff_left IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le pow_zero Finset.range_eq_Ico Finset.insert_Ico_add_one_left_eq_Ico Finset.sum_insert zero_add instCanonicallyOrderedAdd IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add covariant_swap_add_of_covariant_add instNoMaxOrder Finset.sum_congr geom_sum_le mul_add Distrib.leftDistribClass add_tsub_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE instOrderedSub mul_one tsub_pos_of_lt add_comm
geom_sum_le 📖	mathematical	—	Finset.sum instAddCommMonoid Finset.range Monoid.toPow instMonoid	—	tsub_pos_of_lt instCanonicallyOrderedAdd instOrderedSub Finset.sum_range_zero MulZeroClass.zero_mul mul_comm LE.le.trans pred_mul_geom_sum_le tsub_le_self
pred_mul_geom_sum_le 📖	mathematical	—	Finset.sum instAddCommMonoid Finset.range Monoid.toPow instMonoid	—	mul_comm Finset.sum_mul one_mul Finset.sum_range_succ' Finset.sum_range_succ pow_zero add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid Finset.sum_le_sum pow_succ add_tsub_add_eq_tsub_left instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le

Odd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
geom_sum_pos 📖	mathematical	Odd Nat.instSemiring	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.range Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	—	Nat.not_odd_zero Finset.sum_congr zero_add Finset.sum_singleton pow_zero IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero lt_trichotomy geom_sum_alternating_of_lt_neg_one LT.lt.trans zero_lt_one Nat.not_even_iff_odd eq_neg_of_add_eq_zero_left neg_one_geom_sum geom_sum_pos'

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
geom_sum_alternating_of_le_neg_one 📖	mathematical	Preorder.toLE PartialOrder.toPreorder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	Even Nat.instDecidablePredEven Preorder.toLE PartialOrder.toPreorder Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finset.range Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	LE.le.trans le_add_of_nonneg_right IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid zero_le_one IsOrderedRing.toZeroLEOneClass geom_sum_succ le_add_iff_nonneg_left covariant_swap_add_of_covariant_add IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsOrderedAddMonoid.toIsOrderedCancelAddMonoid IsOrderedCancelAddMonoid.toAddLeftReflectLT mul_nonneg_of_nonpos_of_nonpos AddGroup.existsAddOfLE IsOrderedRing.toMulPosMono le_imp_le_of_le_of_le le_refl add_le_add_left mul_one mul_le_mul_of_nonpos_left IsOrderedRing.toPosMulMono
geom_sum_alternating_of_lt_neg_one 📖	mathematical	Preorder.toLT PartialOrder.toPreorder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	Even Nat.instDecidablePredEven Preorder.toLT PartialOrder.toPreorder Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finset.range Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	LE.le.trans_lt le_add_of_nonneg_right IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing zero_le_one IsStrictOrderedRing.toZeroLEOneClass Nat.le_induction geom_sum_two IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsStrictOrderedRing.toIsOrderedCancelAddMonoid IsOrderedCancelAddMonoid.toAddLeftReflectLT covariant_swap_add_of_covariant_add geom_sum_succ lt_add_iff_pos_left mul_pos_of_neg_of_neg AddGroup.existsAddOfLE IsStrictOrderedRing.toMulPosStrictMono lt_imp_lt_of_le_of_le le_refl le_of_lt add_lt_add_left mul_one mul_lt_mul_of_neg_left IsStrictOrderedRing.toPosMulStrictMono
geom_sum_eq_zero_iff_neg_one 📖	mathematical	—	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finset.range Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Even	—	Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_and_eq eq_or_ne neg_one_geom_sum NeZero.charZero_one IsStrictOrderedRing.toCharZero geom_sum_ne_zero Finset.sum_congr
geom_sum_ne_zero 📖	—	—	—	—	Finset.sum_congr zero_add Finset.sum_singleton pow_zero NeZero.charZero_one IsStrictOrderedRing.toCharZero Ne.lt_or_gt eq_neg_iff_add_eq_zero geom_sum_alternating_of_lt_neg_one LT.lt.ne LT.lt.ne' LT.lt.trans zero_lt_one IsStrictOrderedRing.toZeroLEOneClass geom_sum_pos'
geom_sum_neg_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finset.range Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Even Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	not_iff_not not_lt le_iff_lt_or_eq geom_sum_pos_iff geom_sum_eq_zero_iff_neg_one Nat.not_even_iff_odd add_eq_zero_iff_eq_neg imp_iff_not_or
geom_sum_pos 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.range Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Finset.sum_pos' IsStrictOrderedRing.toIsOrderedCancelAddMonoid IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing pow_nonneg IsStrictOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Finset.mem_range Ne.bot_lt pow_zero NeZero.charZero_one IsStrictOrderedRing.toCharZero
geom_sum_pos' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.range Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	—	Finset.sum_congr zero_add Finset.sum_singleton pow_zero IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero lt_or_ge geom_sum_pos_and_lt_one geom_sum_pos
geom_sum_pos_and_lt_one 📖	mathematical	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.range Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	Nat.le_induction geom_sum_two add_lt_iff_neg_right IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsStrictOrderedRing.toIsOrderedCancelAddMonoid IsOrderedCancelAddMonoid.toAddLeftReflectLT covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing geom_sum_succ neg_lt_iff_pos_add' IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono neg_mul_eq_neg_mul mul_lt_one_of_nonneg_of_lt_one_left IsOrderedRing.toPosMulMono neg_nonneg LT.lt.le mul_neg_of_neg_of_pos IsStrictOrderedRing.toMulPosStrictMono
geom_sum_pos_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.range Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Odd Nat.instSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	not_le Nat.not_odd_iff_even LT.lt.not_ge geom_sum_alternating_of_le_neg_one IsStrictOrderedRing.toIsOrderedRing Odd.geom_sum_pos geom_sum_pos'

---

← Back to Index