BigOperators

📁 Source: Mathlib/Data/Complex/BigOperators.lean

Statistics

Metric	Count
Definitions	0
Theorems im_balance, im_comp_balance, im_expect, im_sum, ofReal_balance, ofReal_comp_balance, ofReal_expect, ofReal_prod, ofReal_sum, re_balance, re_comp_balance, re_expect, re_sum	13
Total	13

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
im_balance 📖	mathematical	—	im Fintype.balance Complex addCommGroup Algebra.toModule NNRat instCommSemiringNNRat instSemiring DivisionSemiring.toNNRatAlgebra Semifield.toDivisionSemiring Field.toSemifield instField instCharZero Real Real.instAddCommGroup Real.semiring Real.instField IsStrictOrderedRing.toCharZero DivisionSemiring.toSemiring Real.partialOrder Real.instIsStrictOrderedRing	—	instCharZero IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing im_expect Finset.expect_congr
im_comp_balance 📖	mathematical	—	Complex Real im Fintype.balance addCommGroup Algebra.toModule NNRat instCommSemiringNNRat instSemiring DivisionSemiring.toNNRatAlgebra Semifield.toDivisionSemiring Field.toSemifield instField instCharZero Real.instAddCommGroup Real.semiring Real.instField IsStrictOrderedRing.toCharZero DivisionSemiring.toSemiring Real.partialOrder Real.instIsStrictOrderedRing	—	instCharZero IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing im_balance
im_expect 📖	mathematical	—	im Finset.expect Complex NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing Algebra.toModule NNRat instCommSemiringNNRat instSemiring DivisionSemiring.toNNRatAlgebra Semifield.toDivisionSemiring Field.toSemifield instField instCharZero Real Real.instAddCommMonoid Real.semiring Real.instField IsStrictOrderedRing.toCharZero DivisionSemiring.toSemiring Real.partialOrder Real.instIsStrictOrderedRing	—	map_expect instCharZero IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing LinearMap.semilinearMapClass im_nnqsmul eq_nnratCast RingHom.instRingHomClass
im_sum 📖	mathematical	—	im Finset.sum Complex NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing Real Real.instAddCommMonoid	—	map_sum AddMonoidHom.instAddMonoidHomClass
ofReal_balance 📖	mathematical	—	ofReal Fintype.balance Real Real.instAddCommGroup Algebra.toModule NNRat instCommSemiringNNRat Real.semiring DivisionSemiring.toNNRatAlgebra Semifield.toDivisionSemiring Field.toSemifield Real.instField IsStrictOrderedRing.toCharZero DivisionSemiring.toSemiring Real.partialOrder Real.instIsStrictOrderedRing Complex addCommGroup instSemiring instField instCharZero	—	IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing instCharZero ofReal_sub ofReal_expect Finset.expect_congr
ofReal_comp_balance 📖	mathematical	—	Real Complex ofReal Fintype.balance Real.instAddCommGroup Algebra.toModule NNRat instCommSemiringNNRat Real.semiring DivisionSemiring.toNNRatAlgebra Semifield.toDivisionSemiring Field.toSemifield Real.instField IsStrictOrderedRing.toCharZero DivisionSemiring.toSemiring Real.partialOrder Real.instIsStrictOrderedRing addCommGroup instSemiring instField instCharZero	—	IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing instCharZero ofReal_balance
ofReal_expect 📖	mathematical	—	ofReal Finset.expect Real Real.instAddCommMonoid Algebra.toModule NNRat instCommSemiringNNRat Real.semiring DivisionSemiring.toNNRatAlgebra Semifield.toDivisionSemiring Field.toSemifield Real.instField IsStrictOrderedRing.toCharZero DivisionSemiring.toSemiring Real.partialOrder Real.instIsStrictOrderedRing Complex NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing instSemiring instField instCharZero	—	map_expect IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing instCharZero RingHomClass.toLinearMapClassNNRat RingHom.instRingHomClass
ofReal_prod 📖	mathematical	—	ofReal Finset.prod Real Real.instCommMonoid Complex CommRing.toCommMonoid commRing	—	map_prod MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
ofReal_sum 📖	mathematical	—	ofReal Finset.sum Real Real.instAddCommMonoid Complex NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing	—	map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing instCharZero SemilinearMapClass.distribMulActionSemiHomClass RingHomClass.toLinearMapClassNNRat RingHom.instRingHomClass
re_balance 📖	mathematical	—	re Fintype.balance Complex addCommGroup Algebra.toModule NNRat instCommSemiringNNRat instSemiring DivisionSemiring.toNNRatAlgebra Semifield.toDivisionSemiring Field.toSemifield instField instCharZero Real Real.instAddCommGroup Real.semiring Real.instField IsStrictOrderedRing.toCharZero DivisionSemiring.toSemiring Real.partialOrder Real.instIsStrictOrderedRing	—	instCharZero IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing re_expect Finset.expect_congr
re_comp_balance 📖	mathematical	—	Complex Real re Fintype.balance addCommGroup Algebra.toModule NNRat instCommSemiringNNRat instSemiring DivisionSemiring.toNNRatAlgebra Semifield.toDivisionSemiring Field.toSemifield instField instCharZero Real.instAddCommGroup Real.semiring Real.instField IsStrictOrderedRing.toCharZero DivisionSemiring.toSemiring Real.partialOrder Real.instIsStrictOrderedRing	—	instCharZero IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing re_balance
re_expect 📖	mathematical	—	re Finset.expect Complex NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing Algebra.toModule NNRat instCommSemiringNNRat instSemiring DivisionSemiring.toNNRatAlgebra Semifield.toDivisionSemiring Field.toSemifield instField instCharZero Real Real.instAddCommMonoid Real.semiring Real.instField IsStrictOrderedRing.toCharZero DivisionSemiring.toSemiring Real.partialOrder Real.instIsStrictOrderedRing	—	map_expect instCharZero IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing LinearMap.semilinearMapClass re_nnqsmul eq_nnratCast RingHom.instRingHomClass
re_sum 📖	mathematical	—	re Finset.sum Complex NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing Real Real.instAddCommMonoid	—	map_sum AddMonoidHom.instAddMonoidHomClass

---

← Back to Index