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.toNatPow instMonoid	—	Finset.sum_le_sum_of_subset instCanonicallyOrderedAdd Finset.mem_range geomSum_eq tsub_lt_self instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid
geom_sum_Ico_le 📖	mathematical	—	Finset.sum instAddCommMonoid Finset.Ico instPreorder instLocallyFiniteOrder Monoid.toNatPow instMonoid	—	Finset.Ico_eq_empty_of_le Finset.sum_empty add_le_add_iff_left IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd 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 AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add contravariant_swap_add_of_contravariant_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.toNatPow 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.toNatPow 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 AddLeftCancelSemigroup.toIsLeftCancelAdd 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.toNatPow 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 Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.range Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	—	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 AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add IsOrderedCancelAddMonoid.toAddLeftReflectLT IsOrderedAddMonoid.toIsOrderedCancelAddMonoid 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 Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.range Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	—	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 AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add contravariant_swap_add_of_contravariant_add IsOrderedCancelAddMonoid.toAddLeftReflectLT IsStrictOrderedRing.toIsOrderedCancelAddMonoid 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.toNatPow 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.toNatPow 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 Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.range Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Finset.sum_pos' IsStrictOrderedRing.toIsOrderedCancelAddMonoid pow_nonneg IsStrictOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing 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	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.range Monoid.toNatPow 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	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.range Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	—	Nat.le_induction geom_sum_two add_lt_iff_neg_right IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing contravariant_swap_add_of_contravariant_add IsOrderedCancelAddMonoid.toAddLeftReflectLT IsStrictOrderedRing.toIsOrderedCancelAddMonoid geom_sum_succ neg_lt_iff_pos_add' IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd 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.toNatPow 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