Randomisation

📁 Source: Mathlib/Combinatorics/Additive/Randomisation.lean

Statistics

Metric	Count
Definitions	0
Theorems randomisation	1
Total	1

AddDissociated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
randomisation 📖	mathematical	AddDissociated AddChar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Complex MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring AddChar.instAddCommGroup CommRing.toCommMonoid Complex.commRing setOf Complex.instZero	Finset.expect Real Real.instAddCommMonoid Algebra.toModule NNRat instCommSemiringNNRat Real.semiring DivisionSemiring.toNNRatAlgebra Semifield.toDivisionSemiring Field.toSemifield Real.instField RCLike.charZero_rclike Real.instRCLike Finset.univ Finset.prod Real.instCommMonoid AddChar.instFintype Complex.instRCLike Finite.of_fintype Real.instAdd Complex.re Complex.instMul DFunLike.coe AddChar.instFunLike	—	Complex.ofReal_injective RCLike.charZero_rclike Finite.of_fintype Complex.instCharZero IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Complex.ofReal_expect Finset.expect_congr Complex.ofReal_prod Finset.prod_congr Complex.ofReal_add Nat.instAtLeastTwoHAddOfNat Finset.sum_congr Finset.expect_mul IsScalarTower.right add_comm Complex.re_eq_add_conj Fintype.sum_eq_single mul_eq_zero_of_left map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Finset.prod_div_distrib Finset.prod_add Finset.prod_const Finset.expect_sum_comm isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Complex.instNontrivial Finset.sum_eq_zero Finset.mul_expect Algebra.to_smulCommClass AddChar.sum_apply mul_mul_mul_comm AddChar.map_neg_eq_conj mul_eq_zero AddChar.expect_eq_zero_iff_ne_zero instIsDomain sub_ne_zero mul_ne_zero_iff Finset.prod_ne_zero_iff Set.InjOn.ne RingHomClass.toMonoidWithZeroHomClass sdiff_ne_right pow_zero div_self NeZero.charZero_one Finset.expect_const AddTorsor.nonempty Finset.compl_empty one_mul

---

← Back to Index