Expect

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

Statistics

Metric	Count
Definitions bigexpect, delabFinsetExpect, expect	3
Theorems card_mul_expect, card_smul_expect, exists_ne_zero_of_expect_ne_zero, expectWith_congr, expect_add_distrib, expect_add_expect_comm, expect_apply, expect_bij, expect_bij', expect_boole_mul, expect_boole_mul', expect_comm, expect_congr, expect_const, expect_const_zero, expect_dite_eq, expect_dite_eq', expect_div, expect_empty, expect_eq_single_of_mem, expect_eq_sum_div_card, expect_eq_zero, expect_equiv, expect_image, expect_inv_index, expect_ite_eq, expect_ite_eq', expect_ite_mem, expect_ite_zero, expect_mul, expect_mul_expect, expect_nbij, expect_nbij', expect_neg_distrib, expect_neg_index, expect_pow, expect_product, expect_product', expect_singleton, expect_sub_distrib, expect_sum_comm, expect_univ, mul_expect, smul_expect, card_mul_expect, card_smul_expect, expect_bijective, expect_const, expect_dite_eq, expect_dite_eq', expect_eq_sum_div_card, expect_equiv, expect_ite_eq, expect_ite_eq', expect_ite_mem, expect_ite_zero, expect_mul_expect, expect_one, coe_expect, map_expect	60
Total	63

BigOperators

Definitions

Name	Category	Theorems
bigexpect 📖	CompOp	—
delabFinsetExpect 📖	CompOp	—

Finset

Definitions

Name	Category	Theorems
expect 📖	CompOp	92 math math: expect_ite_mem, expect_congr, AddDissociated.randomisation, le_expect_nonempty_of_subadditive, expect_eq_zero, le_expect_of_subadditive_on_pred, Fintype.expect_mul_expect, RCLike.norm_expect_le, expect_neg_distrib, Fintype.expect_dite_eq, Complex.im_expect, Fintype.expect_eq_zero_iff_of_nonpos, expect_mul_expect, expect_const_zero, expect_comm, Fintype.expect_ite_eq, Fintype.expect_ite_zero, expect_ite_zero, expect_add_distrib, RCLike.wInner_cWeight_eq_expect, Fintype.expect_dite_eq', expect_inv_index, expect_image, le_expect_nonempty_of_subadditive_on_pred, Fintype.expect_eq_zero_iff_of_nonneg, expect_const, Fintype.expect_bijective, AddChar.expect_apply_eq_zero_iff_ne_zero, Fintype.card_mul_expect, expect_empty, expect_eq_zero_iff_of_nonneg, expect_eq_single_of_mem, card_smul_expect, expect_mul, card_mul_expect, Fintype.balance_apply, expect_nbij', expect_sub_distrib, expect_eq_zero_iff_of_nonpos, expect_boole_mul', Fintype.expect_one, expect_add_expect_comm, expect_bij, expect_dite_eq', RCLike.wInner_cWeight_const_left, AddChar.expect_eq_zero_iff_ne_zero, expect_bij', expect_le_expect, expect_mul_sq_le_sq_mul_sq, Complex.ofReal_expect, Fintype.expect_ite_mem, expect_equiv, expect_product, expect_le, expect_nonneg, expect_boole_mul, NNReal.coe_expect, Fintype.expect_balance, RCLike.ofReal_expect, Fintype.expect_equiv, expect_nbij, abs_expect_le, expect_neg_index, mul_expect, expect_univ, expect_dite_eq, expect_apply, Complex.re_expect, smul_expect, RCLike.wInner_cWeight_const_right, expect_div, MeasureTheory.lpNorm_expect_le, Fintype.expect_ite_eq', le_expect, le_expect_of_subadditive, map_expect, Fintype.card_smul_expect, Real.compact_inner_le_weight_mul_Lp_of_nonneg, algebraMap.coe_expect, expect_eq_sum_div_card, AddChar.expect_apply_eq_ite, expect_ite_eq, expect_pow, expect_singleton, expect_sum_comm, expect_ite_eq', expect_pos, AddChar.expect_eq_ite, expect_product', Fintype.expect_const, expectWith_congr, Fintype.expect_eq_sum_div_card

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_mul_expect 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne card expect NonUnitalNonAssocSemiring.toAddCommMonoid sum	—	nsmul_eq_mul card_smul_expect
card_smul_expect 📖	mathematical	—	AddMonoid.toNatSMul AddCommMonoid.toAddMonoid card expect sum	—	eq_empty_or_nonempty expect_empty nsmul_zero expect.eq_1 Nat.cast_smul_eq_nsmul smul_inv_smul₀ Nat.cast_zero NNRat.instCharZero Nonempty.card_ne_zero
exists_ne_zero_of_expect_ne_zero 📖	mathematical	—	Finset instMembership	—	Mathlib.Tactic.Contrapose.contrapose₂ Mathlib.Tactic.Push.not_and_eq expect_eq_zero
expectWith_congr 📖	mathematical	—	expect filter	—	expect_congr filter_inj'
expect_add_distrib 📖	mathematical	—	expect AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	sum_congr sum_add_distrib smul_add
expect_add_expect_comm 📖	mathematical	—	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup expect	—	expect_add_distrib add_add_add_comm
expect_apply 📖	mathematical	—	expect Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.module NNRat DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield	—	sum_congr sum_apply
expect_bij 📖	mathematical	Finset instMembership	expect	—	sum_congr card_bij sum_bij
expect_bij' 📖	mathematical	Finset instMembership	expect	—	sum_congr card_bij' sum_bij'
expect_boole_mul 📖	mathematical	—	expect NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Algebra.toModule NNRat instCommSemiringNNRat DivisionSemiring.toNNRatAlgebra univ Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Fintype.card MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	expect_univ sum_congr ite_mul MulZeroClass.zero_mul sum_ite_eq mem_univ NNRat.cast_natCast NNRat.smul_def inv_smul_smul₀ NNRat.instCharZero
expect_boole_mul' 📖	mathematical	—	expect NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Algebra.toModule NNRat instCommSemiringNNRat DivisionSemiring.toNNRatAlgebra univ Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Fintype.card MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	expect_congr expect_boole_mul
expect_comm 📖	mathematical	—	expect	—	expect.eq_1 expect_sum_comm SMulCommClass.smul_comm smulCommClass_self sum_comm
expect_congr 📖	mathematical	—	expect	—	expect.eq_1 sum_congr
expect_const 📖	mathematical	Nonempty	expect	—	expect.eq_1 sum_const Nat.cast_smul_eq_nsmul inv_smul_smul₀ Nat.cast_zero NNRat.instCharZero Nonempty.card_ne_zero
expect_const_zero 📖	mathematical	—	expect AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	sum_congr sum_const_zero smul_zero
expect_dite_eq 📖	mathematical	—	expect AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finset instMembership decidableMem NNRat SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield Module.toDistribMulAction NNRat.instInv AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring card	—	sum_congr sum_dite_eq smul_zero
expect_dite_eq' 📖	mathematical	—	expect AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finset instMembership decidableMem NNRat SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield Module.toDistribMulAction NNRat.instInv AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring card	—	sum_congr sum_dite_eq' smul_zero
expect_div 📖	mathematical	—	DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring expect NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Algebra.toModule NNRat instCommSemiringNNRat DivisionSemiring.toNNRatAlgebra	—	div_eq_mul_inv expect_congr expect_mul IsScalarTower.right
expect_empty 📖	mathematical	—	expect Finset instEmptyCollection AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Nat.cast_zero inv_zero sum_congr smul_zero
expect_eq_single_of_mem 📖	mathematical	Finset instMembership AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	expect NNRat SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield Module.toDistribMulAction NNRat.instInv AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring card	—	expect.eq_1 sum_eq_single_of_mem
expect_eq_sum_div_card 📖	mathematical	—	expect NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Algebra.toModule NNRat instCommSemiringNNRat DivisionSemiring.toNNRatAlgebra DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero sum AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne card	—	expect.eq_1 NNRat.smul_def div_eq_inv_mul NNRat.cast_inv NNRat.cast_natCast
expect_eq_zero 📖	mathematical	AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	expect	—	expect_congr expect_const_zero
expect_equiv 📖	mathematical	Finset instMembership DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike	expect	—	sum_congr card_equiv sum_equiv
expect_image 📖	mathematical	Set.InjOn SetLike.coe Finset instSetLike	expect image	—	sum_congr card_image_of_injOn sum_image
expect_inv_index 📖	mathematical	—	expect Finset inv InvolutiveInv.toInv	—	expect_image Function.Injective.injOn inv_injective
expect_ite_eq 📖	mathematical	—	expect AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finset instMembership decidableMem NNRat SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield Module.toDistribMulAction NNRat.instInv AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring card	—	sum_congr sum_ite_eq smul_zero
expect_ite_eq' 📖	mathematical	—	expect AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finset instMembership decidableMem NNRat SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield Module.toDistribMulAction NNRat.instInv AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring card	—	sum_congr sum_ite_eq' smul_zero
expect_ite_mem 📖	mathematical	—	expect Finset instMembership decidableMem AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NNRat SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield Module.toDistribMulAction NNRat.instDiv AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring card instInter	—	eq_empty_or_nonempty sum_congr sum_ite_mem smul_zero Nat.cast_zero zero_div inv_zero smul_smul mul_inv_cancel_right₀ NNRat.instCharZero Nonempty.card_ne_zero
expect_ite_zero 📖	mathematical	—	expect AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finset instMembership decidableExistsAndFinset NNRat SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield Module.toDistribMulAction NNRat.instInv AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring card	—	sum_congr sum_ite_zero smul_zero
expect_mul 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring expect NonUnitalNonAssocSemiring.toAddCommMonoid	—	expect.eq_1 smul_mul_assoc sum_mul
expect_mul_expect 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring expect NonUnitalNonAssocSemiring.toAddCommMonoid	—	expect_mul expect_congr mul_expect
expect_nbij 📖	mathematical	Finset instMembership Set.InjOn SetLike.coe instSetLike Set.SurjOn	expect	—	sum_congr card_nbij sum_nbij
expect_nbij' 📖	mathematical	Finset instMembership	expect	—	sum_congr card_nbij' sum_nbij'
expect_neg_distrib 📖	mathematical	—	expect AddCommGroup.toAddCommMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	sum_congr sum_neg_distrib smul_neg
expect_neg_index 📖	mathematical	—	expect Finset neg InvolutiveNeg.toNeg	—	expect_image Function.Injective.injOn neg_injective
expect_pow 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring expect NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Fintype.piFinset Fin.fintype prod CommSemiring.toCommMonoid univ	—	expect.eq_1 smul_pow sum_pow' Fintype.card_piFinset_const inv_pow Nat.cast_pow
expect_product 📖	mathematical	—	expect SProd.sprod Finset instSProd	—	card_product Nat.cast_mul mul_inv sum_congr sum_product smul_sum SemigroupAction.mul_smul
expect_product' 📖	mathematical	—	expect SProd.sprod Finset instSProd	—	card_product Nat.cast_mul mul_inv sum_congr sum_product' smul_sum SemigroupAction.mul_smul
expect_singleton 📖	mathematical	—	expect Finset instSingleton	—	card_singleton Nat.cast_one inv_one sum_congr sum_singleton one_smul
expect_sub_distrib 📖	mathematical	—	expect AddCommGroup.toAddCommMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	sum_congr sum_sub_distrib smul_sub
expect_sum_comm 📖	mathematical	—	expect sum	—	sum_congr smul_sum sum_comm
expect_univ 📖	mathematical	—	expect univ NNRat SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield Module.toDistribMulAction NNRat.instInv AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Fintype.card sum	—	expect.eq_1 card_univ
mul_expect 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring expect NonUnitalNonAssocSemiring.toAddCommMonoid	—	expect.eq_1 mul_smul_comm mul_sum
smul_expect 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass expect	—	sum_congr smul_sum SMulCommClass.smul_comm

Fintype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_mul_expect 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne card Finset.expect NonUnitalNonAssocSemiring.toAddCommMonoid Finset.univ Finset.sum	—	Finset.card_mul_expect
card_smul_expect 📖	mathematical	—	AddMonoid.toNatSMul AddCommMonoid.toAddMonoid card Finset.expect Finset.univ Finset.sum	—	Finset.card_smul_expect
expect_bijective 📖	mathematical	Function.Bijective	Finset.expect Finset.univ	—	Finset.expect_nbij Finset.mem_univ Function.Injective.injOn Function.Bijective.injective Finset.coe_univ Function.Bijective.surjective
expect_const 📖	mathematical	—	Finset.expect Finset.univ	—	Finset.expect_const Finset.univ_nonempty
expect_dite_eq 📖	mathematical	—	Finset.expect Finset.univ AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NNRat SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield Module.toDistribMulAction NNRat.instInv AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring card	—	Finset.expect_dite_eq
expect_dite_eq' 📖	mathematical	—	Finset.expect Finset.univ AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NNRat SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield Module.toDistribMulAction NNRat.instInv AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring card	—	Finset.expect_dite_eq'
expect_eq_sum_div_card 📖	mathematical	—	Finset.expect NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Algebra.toModule NNRat instCommSemiringNNRat DivisionSemiring.toNNRatAlgebra Finset.univ DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero Finset.sum AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne card	—	Finset.expect_eq_sum_div_card
expect_equiv 📖	mathematical	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike	Finset.expect Finset.univ	—	expect_bijective Equiv.bijective
expect_ite_eq 📖	mathematical	—	Finset.expect Finset.univ AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NNRat SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield Module.toDistribMulAction NNRat.instInv AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring card	—	Finset.expect_ite_eq
expect_ite_eq' 📖	mathematical	—	Finset.expect Finset.univ AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NNRat SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield Module.toDistribMulAction NNRat.instInv AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring card	—	Finset.expect_ite_eq'
expect_ite_mem 📖	mathematical	—	Finset.expect Finset.univ Finset Finset.instMembership Finset.decidableMem AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NNRat SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield Module.toDistribMulAction Finset.dens	—	Finset.expect_ite_mem Finset.univ_inter Finset.expect_congr
expect_ite_zero 📖	mathematical	—	Finset.expect Finset.univ AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid decidableExistsFintype NNRat SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield Module.toDistribMulAction NNRat.instInv AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring card	—	Finset.expect_ite_zero
expect_mul_expect 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finset.expect NonUnitalNonAssocSemiring.toAddCommMonoid Finset.univ	—	Finset.expect_mul_expect
expect_one 📖	mathematical	—	Finset.expect NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finset.univ AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	expect_const

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_expect 📖	mathematical	—	DFunLike.coe Finset.expect	—	Finset.sum_congr map_smul SemilinearMapClass.toMulActionSemiHomClass map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass

algebraMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_expect 📖	mathematical	—	Algebra.cast Semifield.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Finset.expect NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule NNRat instCommSemiringNNRat DivisionSemiring.toNNRatAlgebra	—	map_expect RingHomClass.toLinearMapClassNNRat RingHom.instRingHomClass

---

← Back to Index