GeomSum

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

Statistics

Metric	Count
Definitions	0
Theorems geom_sum₂, geom_sum₂_Ico, geom_sum_Ico, geom_sum_Ico', geom_sum_eq, geom_sum_inv, geom_sum₂_Ico, geom₂_sum	8
Total	8

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
geom_sum₂ 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.range Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring DivInvMonoid.toDiv DivisionRing.toDivInvMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	zero_add geom_sum₂_mul mul_div_cancel_right₀ GroupWithZero.toMulDivCancelClass
geom_sum₂_Ico 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.Ico Nat.instPreorder Nat.instLocallyFiniteOrder Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring DivInvMonoid.toDiv DivisionRing.toDivInvMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	zero_add geom_sum₂_Ico_mul mul_div_cancel_right₀ GroupWithZero.toMulDivCancelClass

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
geom_sum_Ico 📖	mathematical	—	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing Finset.Ico Nat.instPreorder Nat.instLocallyFiniteOrder Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring DivInvMonoid.toDiv DivisionRing.toDivInvMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	Finset.sum_Ico_eq_sub geom_sum_eq div_sub_div_same sub_sub_sub_cancel_right
geom_sum_Ico' 📖	mathematical	—	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing Finset.Ico Nat.instPreorder Nat.instLocallyFiniteOrder Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring DivInvMonoid.toDiv DivisionRing.toDivInvMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	geom_sum_Ico neg_sub neg_div_neg_eq
geom_sum_eq 📖	mathematical	—	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing Finset.range Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring DivInvMonoid.toDiv DivisionRing.toDivInvMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	zero_add geom_sum_mul mul_div_cancel_right₀ GroupWithZero.toMulDivCancelClass
geom_sum_inv 📖	mathematical	—	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing Finset.range Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	inv_eq_one_div div_eq_iff_mul_eq one_mul sub_eq_zero pow_zero inv_one mul_one pow_succ' mul_inv_rev mul_assoc mul_inv_cancel₀ inv_mul_cancel₀ geom_sum_eq mul_right_inj' IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero DivisionRing.isDomain inv_pow sub_eq_add_neg mul_add Distrib.leftDistribClass mul_neg add_mul Distrib.rightDistribClass neg_mul add_comm neg_add_rev neg_neg add_left_comm add_assoc
geom_sum₂_Ico 📖	mathematical	—	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Finset.Ico Nat.instPreorder Nat.instLocallyFiniteOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing	—	Commute.geom_sum₂_Ico Commute.all
geom₂_sum 📖	mathematical	—	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 DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing	—	Commute.geom_sum₂ Commute.all

---

← Back to Index