Choose

📁 Source: Mathlib/Analysis/SpecialFunctions/Choose.lean

Statistics

Metric	Count
Definitions	0
Theorems isEquivalent_choose, isEquivalent_descFactorial, isTheta_choose	3
Total	3

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isEquivalent_choose 📖	mathematical	—	Asymptotics.IsEquivalent Real NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Filter.atTop Nat.instPreorder Real.instNatCast Nat.choose DivInvMonoid.toDiv Real.instDivInvMonoid Monoid.toNatPow Real.instMonoid Nat.factorial	—	Nat.choose_eq_descFactorial_div_factorial Nat.cast_div Nat.factorial_dvd_descFactorial Nat.cast_zero IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Nat.factorial_ne_zero Asymptotics.IsEquivalent.div isEquivalent_descFactorial Asymptotics.IsEquivalent.refl
isEquivalent_descFactorial 📖	mathematical	—	Asymptotics.IsEquivalent Real NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Filter.atTop Nat.instPreorder Real.instNatCast Nat.descFactorial Monoid.toNatPow Real.instMonoid	—	Nat.cast_one pow_zero Asymptotics.IsEquivalent.refl Nat.cast_mul pow_succ' Asymptotics.IsEquivalent.mul Filter.eventually_atTop instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat ne_of_gt Nat.cast_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Asymptotics.isEquivalent_iff_tendsto_one Filter.tendsto_add_atTop_iff_nat add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Nat.instIsOrderedAddMonoid Nat.cast_add tendsto_natCast_div_add_atTop NNRat.instContinuousSMulOfIsScalarTowerOfRat IsScalarTower.nnrat Rat.instCharZero NNRat.instContinuousSMulRatReal IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal
isTheta_choose 📖	mathematical	—	Asymptotics.IsTheta Real Real.norm Filter.atTop Nat.instPreorder Real.instNatCast Nat.choose Monoid.toNatPow Real.instMonoid	—	Asymptotics.IsEquivalent.trans_isTheta isEquivalent_choose div_eq_mul_inv mul_comm Asymptotics.IsTheta.const_mul_left inv_ne_zero Nat.cast_zero IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Nat.factorial_ne_zero Asymptotics.isTheta_rfl

---

← Back to Index