factorial 📖 | CompOp | 371 mathmath: Complex.cos_eq_tsum, Lagrange.eval_iterate_derivative_eq_sum, ordinaryHypergeometric_sum_eq, DividedPowers.RatAlgebra.dpow_eq_inv_fact_smul, InnerProductSpace.volume_closedBall_of_dim_even, NormedSpace.expSeries_eq_ofScalars, factorial_mul_ascFactorial, cast_factorial, taylorWithinEval_hasDerivAt_Ioo, cast_choose_eq_ascPochhammer_div, Stirling.factorial_isEquivalent_stirling, choose_eq_asc_factorial_div_factorial', PeriodPair.iteratedDeriv_weierstrassPExcept_self, Complex.Gamma_nat_eq_factorial, DividedPowers.factorial_mul_dpow_eq_pow, hasDerivWithinAt_taylorWithinEval, Complex.hasSum_taylorSeries_of_entire, norm_iteratedFDeriv_comp_le', Equiv.Perm.card_of_cycleType_mul_eq, ascPochhammer_eval_one, hasSum_one_div_nat_pow_mul_fourier, norm_iteratedFDerivWithin_comp_le_aux, Polynomial.aeval_iterate_derivative_of_ge, Prime.coprime_factorial_of_lt, HurwitzZeta.cosZeta_two_mul_nat, uniformBell_eq_div, prod_range_factorial_succ, Polynomial.iterate_derivative_eq_factorial_smul_sum, factorial_dvd_ascFactorial, ZMod.wilsons_lemma, LiouvilleNumber.partialSum_eq_rat, PeriodPair.iteratedDeriv_derivWeierstrassPExcept_self, sub_one_mul_padicValNat_factorial, Complex.hasSum_taylorSeries_on_ball, NormedSpace.exp_series_hasSum_exp', Fintype.card_perm, NumberField.abs_discr_ge', Complex.taylorSeries_eq_of_entire, factorialBinarySplitting.factorial_mul_prodRange, Matrix.det_le, Equiv.Perm.OnCycleFactors.kerParam_range_card, dvd_factorial, Polynomial.aeval_sumIDeriv, Ring.choose_eq_smul, Stirling.log_stirlingSeq_formula, Polynomial.aeval_iterate_derivative_self, Real.exp_bound, Fintype.card_equiv, factorial_mul_factorial_dvd_factorial_add, prod_factorial_pos, HasFPowerSeriesOnBall.hasSum_iteratedFDeriv, factorization_factorial, NormedSpace.expSeries_apply_eq_div', Prime.emultiplicity_factorial, Real.hasSum_sinh, LiouvilleNumber.aux_calc, Polynomial.bernoulli_generating_function, uniformBell_mul_eq, Complex.taylorSeries_eq_on_ball', fourierCoeff_bernoulli_eq, factorial_succ, AnalyticAt.exists_eventuallyEq_sum_add_pow_mul, Prime.dvd_factorial, FloorSemiring.tendsto_mul_pow_div_factorial_sub_atTop, Equiv.Perm.OnCycleFactors.nat_card_range_toPermHom, LindemannWeierstrass.exp_polynomial_approx, Real.hasSum_cosh, NormedSpace.exp_eq_tsum, padicValNat_mul_div_factorial, card_perm, Stirling.le_log_factorial_stirling, eventually_pow_lt_factorial_sub, NormedSpace.exp_eq_tsum_div, Real.exp_sub_sum_range_succ_isLittleO_pow, descPochhammer_eval_div_factorial_le_sum_choose, Prime.emultiplicity_factorial_mul, IsNilpotent.exp_smul_eq_sum, LiouvilleNumber.summable, Real.hasSum_cos, iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_div_pow, Real.BohrMollerup.f_nat_eq, NormedSpace.expSeries_sum_eq, FloorSemiring.tendsto_pow_div_factorial_atTop, Complex.cos_eq_tsum', taylor_mean_remainder_lagrange_iteratedDeriv, AlternatingGroup.card_of_cycleType_singleton, isEquivalent_choose, ODE.FunSpace.dist_iterate_iterate_next_le_of_lipschitzWith, multinomial_univ_two, Real.expNear_sub, IsUnit.natCast_factorial_iff_of_charP, Real.deriv_Gamma_nat, PadicInt.norm_ascPochhammer_le, Quaternion.expSeries_odd_of_imaginary, NormedSpace.norm_expSeries_summable_of_mem_ball', Multiset.bell_mul_eq, Matrix.det_sum_le, factorial_eq_one, Stirling.le_factorial_stirling, ordinaryHypergeometricSeries_apply_eq', LiouvilleNumber.remainder_summable, Complex.norm_exp_sub_sum_le_norm_mul_exp, Polynomial.exists_iterate_derivative_eq_factorial_smul, Complex.deriv_Gamma_nat, cast_add_choose, Equiv.Perm.card_isConj_eq, Real.sum_le_exp_of_nonneg, Prime.pow_dvd_factorial_iff, DiffContOnCl.circleIntegral_one_div_sub_center_pow_smul, Complex.isCauSeq_norm_exp, MultilinearMap.domCoprod_alternization_eq, Complex.hasSum_sin, Real.sin_eq_tsum, NormedSpace.expSeries_summable', taylor_mean_remainder, factorial_eq_mul_doubleFactorial, EisensteinSeries.q_expansion_riemannZeta, Ring.factorial_nsmul_multichoose_eq_ascPochhammer, Real.sinh_eq_tsum, NormedSpace.expSeries_div_hasSum_exp_of_mem_ball, Real.cos_eq_tsum, Equiv.Perm.card_of_cycleType, PowerSeries.exp_pow_sum, hasDerivWithinAt_taylorWithinEval_at_Icc, NormedSpace.expSeries_apply_eq, eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet, hasSum_one_div_nat_pow_mul_cos, emultiplicity_two_factorial_lt, DividedPowers.RatAlgebra.dpow_apply, choose_mul_factorial_mul_factorial, List.length_permutations, hasDerivWithinAt_taylor_coeff_within, eqOn_iteratedDeriv_cotTerm, one_ascFactorial, Quaternion.expSeries_even_of_imaginary, NormedSpace.expSeries_div_summable, factorial_mul_pow_le_factorial, ordinaryHypergeometric_eq_tsum, NormedSpace.expSeries_apply_eq_div, ascFactorial_eq_factorial_mul_choose', choose_lt_pow_div, prod_factorial_dvd_factorial_sum, iteratedDerivWithin_one_div, ModularFormClass.qExpansion_coeff, cast_choose_eq_descPochhammer_div, Complex.cosh_eq_tsum, Polynomial.eval_iterate_derivative_rootMultiplicity, PowerSeries.coeff_exp, ProbabilityTheory.hasFPowerSeriesAt_mgf, taylorWithinEval_succ, length_permsOfList, prod_Icc_factorial, AlternatingGroup.card_of_cycleType, padicValNat_factorial_le, ascFactorial_eq_div', Ring.ascPochhammer_succ_succ, bernoulliFourierCoeff_eq, Lagrange.iterate_derivative_interpolate, Finset.prod_Ico_id_eq_factorial, iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_zpow, ordinaryHypergeometricSeries_apply_eq, BinomialRing.factorial_nsmul_multichoose, Finset.prod_range_add_one_eq_factorial, descFactorial_eq_div, Complex.norm_iteratedDeriv_le_of_forall_mem_sphere_norm_le, multinomial_spec, factorial_mul_factorial_dvd_factorial, Real.Gamma_ofNat_eq_factorial, Function.mem_periodicPts_iff_isPeriodicPt_factorial_card, card_perms_of_finset, sub_one_mul_padicValNat_factorial_lt_of_ne_zero, factorial_inj, Complex.hasSum_taylorSeries_on_emetric_ball, prime_iff_fac_equiv_neg_one, monotone_factorial, NormedSpace.norm_expSeries_summable', DomMulAct.stabilizer_card', NormedSpace.norm_expSeries_div_summable_of_mem_ball, add_factorial_succ_lt_factorial_add_succ, factorial_le_pow, EisensteinSeries.qExpansion_identity_pnat, factorial_dvd_factorial, two_pow_mul_factorial_le_factorial_two_mul, NormedSpace.expSeries_apply_eq', add_factorial_succ_le_factorial_add_succ, IsUnit.natCast_factorial_of_algebra, Complex.hasSum_cos', one_lt_factorial, factorial_dvd_descFactorial, HasFPowerSeriesOnBall.factorial_smul, Polynomial.iterate_derivative_prod_X_sub_C, factorial_tendsto_atTop, factorial_two, Complex.exp_sub_sum_range_succ_isLittleO_pow, Real.pow_div_factorial_le_exp, Function.injective_iff_iterate_factorial_card_eq_id, Function.isPeriodicPt_factorial_card_of_mem_periodicPts, Polynomial.factorial_mul_shiftedLegendre_eq, AlternatingMap.coe_alternatization, NormedSpace.expSeries_div_summable_of_mem_ball, Polynomial.leadingCoeff_preHilbertPoly, ascFactorial_eq_div, AnalyticAt.hasFPowerSeriesAt, fwdDiff_iter_eq_factorial, Complex.exp_sub_sum_range_isBigO_pow, padicValNat_factorial, MulAction.IsMultiplyPretransitive.index_of_fixingSubgroup_eq, superFactorial_two_mul, AnalyticAt.exists_eq_sum_add_pow_mul, Complex.exp_bound, Complex.taylorSeries_eq_on_eball, numDerangements_tendsto_inv_e, Polynomial.eval_sumIDeriv_of_pos, norm_iteratedFDerivWithin_comp_le, ODE.FunSpace.dist_iterate_next_le, ZMod.cast_descFactorial, card_alternatingGroup, HurwitzZeta.sinZeta_two_mul_nat_add_one, Multiset.bell_eq, NumberField.exists_ideal_in_class_of_norm_le, Real.summable_pow_div_factorial, DividedPowers.OfInvertibleFactorial.dpow_eq_of_mem, norm_iteratedFDeriv_comp_le, ODE.FunSpace.dist_iterate_next_iterate_next_le, iter_deriv_inv, IsNilpotent.exp_eq_sum, iter_deriv_inv', FloorSemiring.eventually_mul_pow_lt_factorial_sub, Complex.sinh_eq_tsum, choose_eq_asc_factorial_div_factorial, Polynomial.factorial_smul_hasseDeriv, NumberField.exists_ne_zero_mem_ringOfIntegers_of_norm_le_mul_sqrt_discr, List.length_permutationsAux, Complex.taylorSeries_eq_on_emetric_ball, ascFactorial_eq_factorial_mul_choose, Complex.sin_eq_tsum, eventually_mul_pow_lt_factorial_sub, hasSum_one_div_nat_pow_mul_sin, Prime.emultiplicity_factorial_le_div_pred, Real.Wallis.W_eq_factorial_ratio, DividedPowers.RatAlgebra.dpow_eq_of_mem, Complex.taylorSeries_eq_on_ball, Complex.exp_bound', stirlingFirst_one_right, NormedSpace.expSeries_sum_eq_div, NormedSpace.expSeries_div_hasSum_exp, NumberField.abs_discr_ge_of_isTotallyComplex, coprime_factorial_iff, superFactorial_succ, choose_le_pow_div, LiouvilleNumber.partialSum_succ, factorial_le, Prime.multiplicity_factorial_pow, Polynomial.iterate_derivative_X_sub_pow_self, factorization_factorial_mul_succ, factorial_mul_pow_sub_le_factorial, Complex.circleIntegral_one_div_sub_center_pow_smul_of_differentiable_on_off_countable, Polynomial.fwdDiff_iter_degree_eq_factorial, EisensteinSeries.qExpansion_identity, padicValNat_factorial_lt_of_ne_zero, Real.hasSum_sin, tsum_eisSummand_eq_tsum_sigma_mul_cexp_pow, descFactorial_self, add_choose, iteratedDerivWithin_cot_sub_inv_eq_add_mul_tsum, self_le_factorial, sub_one_mul_factorization_factorial, iter_deriv_inv_linear_sub, Complex.taylorSeries_eq_on_eball', Real.exp_bound', doubleFactorial_two_mul, LaurentSeries.derivative_iterate, pow_le_choose, factorial_eq_factorialBinarySplitting, doubleFactorial_le_factorial, Matrix.det_sum_smul_le, factorial_mul_ascFactorial', factorization_factorial_le_div_pred, NumberField.abs_discr_rpow_ge_of_isTotallyComplex, factorial_zero, add_choose_mul_factorial_mul_factorial, NormedSpace.norm_expSeries_div_summable, summable_bernoulli_fourier, factorial_lt_of_lt, Ring.descPochhammer_eq_factorial_smul_choose, Complex.hasSum_sinh, Complex.norm_exp_sub_sum_le_exp_norm_sub_sum, taylor_mean_remainder_cauchy, iteratedDeriv_fun_pow_zero, Real.exp_approx_end, factorial_coe_dvd_prod, superFactorial_four_mul, iter_deriv_inv_linear, Complex.hasSum_sin', Numbering.card_prefixed, NormedSpace.exp_eq_tsum_rat, taylor_mean_remainder_bound, hasSum_one_div_pow_mul_fourier_mul_bernoulliFun, Complex.sin_eq_tsum', Complex.betaIntegral_eval_nat_add_one_right, Prime.emultiplicity_factorial_mul_succ, NumberField.exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr, Real.exp_approx_end', DomMulAct.stabilizer_ncard, Mathlib.Meta.NormNum.isNat_factorial, add_factorial_le_factorial_add, cast_choose, NormedSpace.expSeries_hasSum_exp_of_mem_ball', binomial_spec, choose_eq_descFactorial_div_factorial, factorial_lt, descFactorial_eq_factorial_mul_choose, padicValNat_factorial_mul_add, DifferentiableOn.circleIntegral_one_div_sub_center_pow_smul, Complex.hasSum_cosh, Complex.taylorSeries_eq_of_entire', Equiv.Perm.card_of_cycleType_singleton, Complex.Gamma_ofNat_eq_factorial, Real.cosh_eq_tsum, factorial_pos, Real.Gamma_nat_eq_factorial, riemannZeta_two_mul_nat, Real.hasDerivAt_Gamma_nat, hasSum_zeta_nat, padicValNat_factorial_mul, Complex.hasSum_cos, NormedSpace.expSeries_summable_of_mem_ball', eqOn_iteratedDerivWithin_cotTerm_integerComplement, nat_card_alternatingGroup, lt_factorial_self, LiouvilleNumber.remainder_lt, Complex.isCauSeq_exp, taylor_mean_remainder_lagrange, Ring.smeval_ascPochhammer_self_neg, PadicInt.coe_dpow_eq, tendsto_factorial_div_pow_self_atTop, Fintype.card_numbering, DomMulAct.stabilizer_card, factorial_eq_prod_range_add_one, factorial_inj', Real.exp_sub_sum_range_isBigO_pow, taylor_within_apply, Complex.sum_div_factorial_le, IsUnit.natCast_factorial_of_isNilpotent, InnerProductSpace.volume_ball_of_dim_even, binomial_eq, ODE.FunSpace.dist_iterate_next_apply_le, AlternatingGroup.card_of_cycleType_mul_eq, Polynomial.coeff_preHilbertPoly_self, Equiv.Perm.card_isConj_mul_eq, multinomial_univ_three, mul_factorial_pred, Complex.taylorSeries_eq_on_emetric_ball', Prime.sub_one_mul_multiplicity_factorial, Equiv.Perm.nat_card_centralizer, factorial_two_mul_le, LiouvilleNumber.remainder_lt', add_factorial_lt_factorial_add, factorial_one, factorization_factorial_mul, Complex.hasDerivAt_Gamma_nat, factorial_mul_descFactorial, choose_eq_factorial_div_factorial, MulAction.IsMultiplyPretransitive.index_of_fixingSubgroup_mul, prod_range_succ_factorial, Complex.hasSum_taylorSeries_on_eball, factorial_mul_ascPochhammer, Polynomial.aeval_sumIDeriv_of_pos, factorialBinarySplitting_eq_factorial, factorization_factorial_eq_zero_of_lt, NormedSpace.exp_eq_ofScalarsSum
|