Ring

📁 Source: Mathlib/Topology/Algebra/InfiniteSum/Ring.lean

Statistics

Metric	Count
Definitions	0
Theorems tsum_left, tsum_right, const_div, div_const, mul, mul_eq, mul_left, mul_right, const_div, div_const, mul_left, mul_right, one_sub_mul_tsum_pow, tsum_mul_left, tsum_mul_right, tsum_mul_tsum, tsum_mul_tsum_eq_tsum_sum_antidiagonal, tsum_mul_tsum_eq_tsum_sum_range, tsum_pow_mul_one_sub, hasProd_one_add_of_hasSum_prod, hasSum_const_div_iff, hasSum_div_const_iff, hasSum_mul_left_iff, hasSum_mul_right_iff, multipliable_one_add_of_summable_prod, summable_const_div_iff, summable_div_const_iff, summable_mul_left_iff, summable_mul_prod_iff_summable_mul_sigma_antidiagonal, summable_mul_right_iff, summable_sum_mul_antidiagonal_of_summable_mul, summable_sum_mul_range_of_summable_mul, tprod_one_add, tprod_one_add_ordered, tprod_one_sub_ordered, tsum_div_const, tsum_mul_left, tsum_mul_right	38
Total	38

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tsum_left 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib tsum NonUnitalNonAssocSemiring.toAddCommMonoid	—	symm tsum_right
tsum_right 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib tsum NonUnitalNonAssocSemiring.toAddCommMonoid	—	Summable.tsum_mul_left tsum_congr Summable.tsum_mul_right zero_right tsum_eq_zero_of_not_summable

HasSum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
const_div 📖	mathematical	HasSum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	HasSum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	mul_left div_eq_mul_inv one_mul
div_const 📖	mathematical	HasSum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring	HasSum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero	—	div_eq_mul_inv mul_right
mul 📖	mathematical	HasSum NonUnitalNonAssocSemiring.toAddCommMonoid SummationFilter.unconditional Summable Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	HasSum NonUnitalNonAssocSemiring.toAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SummationFilter.unconditional	—	mul_eq
mul_eq 📖	mathematical	HasSum NonUnitalNonAssocSemiring.toAddCommMonoid SummationFilter.unconditional Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	mul_right mul_left prod_fiberwise IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring T3Space.toRegularSpace unique T25Space.t2Space T3Space.t25Space SummationFilter.instNeBotUnconditional
mul_left 📖	mathematical	HasSum NonUnitalNonAssocSemiring.toAddCommMonoid	HasSum NonUnitalNonAssocSemiring.toAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	map AddMonoidHom.instAddMonoidHomClass Continuous.mul IsTopologicalSemiring.toContinuousMul continuous_const continuous_id
mul_right 📖	mathematical	HasSum NonUnitalNonAssocSemiring.toAddCommMonoid	HasSum NonUnitalNonAssocSemiring.toAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	map AddMonoidHom.instAddMonoidHomClass Continuous.mul IsTopologicalSemiring.toContinuousMul continuous_id continuous_const

Summable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
const_div 📖	mathematical	Summable NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	Summable NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero	—	HasSum.summable HasSum.const_div hasSum
div_const 📖	mathematical	Summable NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring	Summable NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero	—	HasSum.summable HasSum.div_const hasSum
mul_left 📖	mathematical	Summable NonUnitalNonAssocSemiring.toAddCommMonoid	Summable NonUnitalNonAssocSemiring.toAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	HasSum.summable HasSum.mul_left hasSum
mul_right 📖	mathematical	Summable NonUnitalNonAssocSemiring.toAddCommMonoid	Summable NonUnitalNonAssocSemiring.toAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	HasSum.summable HasSum.mul_right hasSum
one_sub_mul_tsum_pow 📖	mathematical	Summable NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SummationFilter.unconditional	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne tsum NonUnitalNonAssocSemiring.toAddCommMonoid Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SummationFilter.unconditional	—	tendsto_nhds_unique Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat HasSum.tendsto_sum_nat HasSum.mul_left IsTopologicalRing.toIsTopologicalSemiring hasSum mul_neg_geom_sum sub_zero Filter.Tendsto.sub IsTopologicalAddGroup.to_continuousSub IsSemitopologicalRing.toIsTopologicalAddGroup IsTopologicalRing.toIsSemitopologicalRing tendsto_const_nhds tendsto_atTop_zero
tsum_mul_left 📖	mathematical	Summable NonUnitalNonAssocSemiring.toAddCommMonoid	tsum NonUnitalNonAssocSemiring.toAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	HasSum.tsum_eq HasSum.mul_left hasSum
tsum_mul_right 📖	mathematical	Summable NonUnitalNonAssocSemiring.toAddCommMonoid	tsum NonUnitalNonAssocSemiring.toAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	HasSum.tsum_eq HasSum.mul_right hasSum
tsum_mul_tsum 📖	mathematical	Summable NonUnitalNonAssocSemiring.toAddCommMonoid SummationFilter.unconditional Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib tsum NonUnitalNonAssocSemiring.toAddCommMonoid SummationFilter.unconditional	—	HasSum.mul_eq hasSum
tsum_mul_tsum_eq_tsum_sum_antidiagonal 📖	mathematical	Summable NonUnitalNonAssocSemiring.toAddCommMonoid SummationFilter.unconditional Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib tsum NonUnitalNonAssocSemiring.toAddCommMonoid SummationFilter.unconditional Finset.sum Finset.HasAntidiagonal.antidiagonal AddCommMonoid.toAddMonoid	—	Finset.sum_finset_coe tsum_fintype SummationFilter.instLeAtTopUnconditional tsum_mul_tsum Equiv.tsum_eq tsum_sigma' IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring HasSum.summable hasSum_fintype summable_mul_prod_iff_summable_mul_sigma_antidiagonal
tsum_mul_tsum_eq_tsum_sum_range 📖	mathematical	Summable NonUnitalNonAssocSemiring.toAddCommMonoid SummationFilter.unconditional Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib tsum NonUnitalNonAssocSemiring.toAddCommMonoid SummationFilter.unconditional Finset.sum Finset.range	—	Finset.Nat.sum_antidiagonal_eq_sum_range_succ tsum_mul_tsum_eq_tsum_sum_antidiagonal
tsum_pow_mul_one_sub 📖	mathematical	Summable NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SummationFilter.unconditional	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing tsum NonUnitalNonAssocSemiring.toAddCommMonoid Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SummationFilter.unconditional SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	tendsto_nhds_unique Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat HasSum.tendsto_sum_nat HasSum.mul_right IsTopologicalRing.toIsTopologicalSemiring hasSum geom_sum_mul_neg sub_zero Filter.Tendsto.sub IsTopologicalAddGroup.to_continuousSub IsSemitopologicalRing.toIsTopologicalAddGroup IsTopologicalRing.toIsSemitopologicalRing tendsto_const_nhds tendsto_atTop_zero

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasProd_one_add_of_hasSum_prod 📖	mathematical	HasSum Finset NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finset.prod CommSemiring.toCommMonoid SummationFilter.unconditional	HasProd CommSemiring.toCommMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne SummationFilter.unconditional	—	Finset.prod_congr Finset.prod_one_add Filter.Tendsto.comp Filter.tendsto_finset_powerset_atTop_atTop
hasSum_const_div_iff 📖	mathematical	—	HasSum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Pi.instDiv Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	div_eq_mul_inv one_mul hasSum_mul_left_iff
hasSum_div_const_iff 📖	mathematical	—	HasSum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero	—	div_eq_mul_inv hasSum_mul_right_iff inv_ne_zero
hasSum_mul_left_iff 📖	mathematical	—	HasSum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	inv_mul_cancel_left₀ HasSum.mul_left
hasSum_mul_right_iff 📖	mathematical	—	HasSum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	mul_inv_cancel_right₀ HasSum.mul_right
multipliable_one_add_of_summable_prod 📖	mathematical	Summable Finset NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finset.prod CommSemiring.toCommMonoid SummationFilter.unconditional	Multipliable CommSemiring.toCommMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne SummationFilter.unconditional	—	hasProd_one_add_of_hasSum_prod
summable_const_div_iff 📖	mathematical	—	Summable NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero Pi.instDiv Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	div_eq_mul_inv one_mul summable_mul_left_iff
summable_div_const_iff 📖	mathematical	—	Summable NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero	—	div_eq_mul_inv summable_mul_right_iff inv_ne_zero
summable_mul_left_iff 📖	mathematical	—	Summable NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	inv_mul_cancel_left₀ Summable.mul_left
summable_mul_prod_iff_summable_mul_sigma_antidiagonal 📖	mathematical	—	Summable NonUnitalNonAssocSemiring.toAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SummationFilter.unconditional Finset SetLike.instMembership Finset.instSetLike Finset.HasAntidiagonal.antidiagonal AddCommMonoid.toAddMonoid	—	Equiv.summable_iff
summable_mul_right_iff 📖	mathematical	—	Summable NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	mul_inv_cancel_right₀ Summable.mul_right
summable_sum_mul_antidiagonal_of_summable_mul 📖	mathematical	Summable NonUnitalNonAssocSemiring.toAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SummationFilter.unconditional	Summable NonUnitalNonAssocSemiring.toAddCommMonoid Finset.sum Finset.HasAntidiagonal.antidiagonal AddCommMonoid.toAddMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SummationFilter.unconditional	—	Finset.sum_finset_coe tsum_fintype SummationFilter.instLeAtTopUnconditional Summable.sigma' IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring T3Space.toRegularSpace summable_mul_prod_iff_summable_mul_sigma_antidiagonal HasSum.summable hasSum_fintype
summable_sum_mul_range_of_summable_mul 📖	mathematical	Summable NonUnitalNonAssocSemiring.toAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SummationFilter.unconditional	Summable NonUnitalNonAssocSemiring.toAddCommMonoid Finset.sum Finset.range Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SummationFilter.unconditional	—	Finset.Nat.sum_antidiagonal_eq_sum_range_succ summable_sum_mul_antidiagonal_of_summable_mul
tprod_one_add 📖	mathematical	Summable Finset NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finset.prod CommSemiring.toCommMonoid SummationFilter.unconditional	tprod CommSemiring.toCommMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne SummationFilter.unconditional tsum Finset NonUnitalNonAssocSemiring.toAddCommMonoid Finset.prod	—	HasProd.tprod_eq SummationFilter.instNeBotUnconditional hasProd_one_add_of_hasSum_prod Summable.hasSum
tprod_one_add_ordered 📖	mathematical	Summable NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Finset.prod CommSemiring.toCommMonoid Finset.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toAdd AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne SummationFilter.unconditional Multipliable	tprod CommSemiring.toCommMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne SummationFilter.unconditional tsum NonUnitalNonAssocSemiring.toAddCommMonoid Distrib.toMul Finset.prod Finset.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	isEmpty_or_nonempty tprod_empty tsum_empty add_zero HasSum.tsum_eq SummationFilter.instNeBotUnconditional tendsto_nhds_unique Filter.atTop_neBot SemilatticeSup.instIsDirectedOrder Filter.Tendsto.comp Finset.prod_one_add_ordered Filter.tendsto_finset_Iic_atTop_atTop Filter.Tendsto.const_add instSeparatelyContinuousAddOfContinuousAdd Finset.sum_congr HasProd.tprod_eq
tprod_one_sub_ordered 📖	mathematical	Summable NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Finset.prod CommRing.toCommMonoid Finset.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne SummationFilter.unconditional Multipliable	tprod CommRing.toCommMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne SummationFilter.unconditional tsum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Finset.prod Finset.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	sub_eq_add_neg Finset.prod_congr tprod_one_add_ordered IsTopologicalAddGroup.toContinuousAdd Summable.neg
tsum_div_const 📖	mathematical	—	tsum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero	—	div_eq_mul_inv tsum_mul_right
tsum_mul_left 📖	mathematical	—	tsum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	MulZeroClass.zero_mul tsum_zero Topology.IsClosedEmbedding.map_tsum AddMonoidHom.instAddMonoidHomClass Homeomorph.isClosedEmbedding IsSemitopologicalSemiring.toSeparatelyContinuousMul IsTopologicalSemiring.toIsSemitopologicalSemiring
tsum_mul_right 📖	mathematical	—	tsum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	MulZeroClass.mul_zero tsum_zero Topology.IsClosedEmbedding.map_tsum AddMonoidHom.instAddMonoidHomClass Homeomorph.isClosedEmbedding IsSemitopologicalSemiring.toSeparatelyContinuousMul IsTopologicalSemiring.toIsSemitopologicalSemiring

---

← Back to Index