Field

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

Statistics

Metric	Count
Definitions	0
Theorems dens_biUnion, dens_biUnion_le, dens_disjiUnion, dens_eq_sum_dens_fiberwise, dens_eq_sum_dens_image, sum_div, sum_map_div	7
Total	7

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dens_biUnion 📖	mathematical	Set.PairwiseDisjoint Finset partialOrder instOrderBot SetLike.coe instSetLike	dens biUnion sum NNRat NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield	—	card_biUnion Nat.cast_sum sum_div sum_congr
dens_biUnion_le 📖	mathematical	—	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat dens biUnion sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield	—	sum_congr div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono instIsStrictOrderedRingNNRat IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass NNRat.instCharZero card_biUnion_le Nat.cast_nonneg'
dens_disjiUnion 📖	mathematical	Set.PairwiseDisjoint Finset partialOrder instOrderBot SetLike.coe instSetLike	dens disjiUnion sum NNRat NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield	—	card_disjiUnion Nat.cast_sum sum_div sum_congr
dens_eq_sum_dens_fiberwise 📖	mathematical	Set.MapsTo SetLike.coe Finset instSetLike	dens sum NNRat NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield filter	—	card_eq_sum_card_fiberwise Nat.cast_sum sum_congr
dens_eq_sum_dens_image 📖	mathematical	—	dens sum NNRat NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield image filter	—	dens_eq_sum_dens_fiberwise mem_image_of_mem
sum_div 📖	mathematical	—	DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring	—	div_eq_mul_inv sum_mul sum_congr

Multiset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sum_map_div 📖	mathematical	—	sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring map DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero	—	map_congr div_eq_mul_inv sum_map_mul_right

---

← Back to Index