Bernoulli

📁 Source: Mathlib/NumberTheory/Bernoulli.lean

Statistics

Metric	Count
Definitions bernoulli, bernoulli', bernoulli'PowerSeries, bernoulliPowerSeries	4
Theorems bernoulli'PowerSeries_mul_exp_sub_one, bernoulli'_def, bernoulli'_def', bernoulli'_eq_bernoulli, bernoulli'_eq_zero_of_odd, bernoulli'_four, bernoulli'_odd_eq_zero, bernoulli'_one, bernoulli'_spec, bernoulli'_spec', bernoulli'_three, bernoulli'_two, bernoulli'_zero, bernoulliPowerSeries_mul_exp_sub_one, bernoulli_eq_bernoulli'_of_ne_one, bernoulli_eq_zero_of_odd, bernoulli_one, bernoulli_spec', bernoulli_two, bernoulli_zero, sum_Ico_pow, sum_bernoulli, sum_bernoulli', sum_range_pow	24
Total	28

(root)

Definitions

Name	Category	Theorems
bernoulli 📖	CompOp	20 math math: Polynomial.bernoulli_succ_eval, Polynomial.bernoulli_eval_zero, Polynomial.sum_range_pow_eq_bernoulli_sub, bernoulli_spec', bernoulli_zero, bernoulli_eq_zero_of_odd, bernoulliFun_eval_zero, Polynomial.bernoulli_def, bernoulli'_eq_bernoulli, EisensteinSeries.q_expansion_bernoulli, bernoulli_two, sum_range_pow, bernoulli_eq_bernoulli'_of_ne_one, Polynomial.coeff_bernoulli, sum_bernoulli, riemannZeta_neg_nat_eq_bernoulli, riemannZeta_two_mul_nat, hasSum_zeta_nat, bernoulli_one, bernoulliFun_eval_half
bernoulli' 📖	CompOp	17 math math: Polynomial.bernoulli_eval_one, bernoulli'_two, bernoulli'_spec, bernoulli'_spec', sum_Ico_pow, bernoulli'_three, sum_bernoulli', bernoulli'_eq_bernoulli, bernoulli'_four, bernoulli'_odd_eq_zero, bernoulli'_one, bernoulli_eq_bernoulli'_of_ne_one, bernoulli'_def, riemannZeta_neg_nat_eq_bernoulli', bernoulli'_eq_zero_of_odd, bernoulli'_def', bernoulli'_zero
bernoulli'PowerSeries 📖	CompOp	1 math math: bernoulli'PowerSeries_mul_exp_sub_one
bernoulliPowerSeries 📖	CompOp	1 math math: bernoulliPowerSeries_mul_exp_sub_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bernoulli'PowerSeries_mul_exp_sub_one 📖	mathematical	—	PowerSeries MvPowerSeries.instMul CommSemiring.toSemiring CommRing.toCommSemiring bernoulli'PowerSeries SubNegMonoid.toSub AddGroup.toSubNegMonoid PowerSeries.instAddGroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing PowerSeries.exp MvPowerSeries.instOne PowerSeries.X	—	PowerSeries.ext PowerSeries.coeff_zero_eq_constantCoeff map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_sub RingHomClass.toAddMonoidHomClass PowerSeries.constantCoeff_exp sub_self MulZeroClass.mul_zero PowerSeries.constantCoeff_X mul_one bernoulli'PowerSeries.eq_1 PowerSeries.coeff_mul mul_comm Finset.Nat.sum_antidiagonal_succ' eq_inv_of_mul_eq_one_left Finset.sum_mul Finset.sum_congr Nat.factorial_mul_factorial_dvd_factorial_add mul_inv_rev Nat.add_choose Nat.cast_div_charZero Rat.instCharZero Nat.cast_mul Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ div_one Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.cons_ne_zero ne_of_gt Nat.cast_pos' Rat.instAddLeftMono Rat.instZeroLEOneClass NeZero.charZero_one Nat.factorial_pos Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add Nat.cast_nonneg' Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Rat.instIsStrictOrderedRing Rat.nontrivial Mathlib.Meta.NormNum.isNat_ofNat one_ne_zero NeZero.one GroupWithZero.toNontrivial bernoulli'_spec' Nat.cast_add Nat.cast_one DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass PowerSeries.coeff_exp one_div PowerSeries.coeff_one sub_zero zero_add PowerSeries.coeff_succ_mul_X map_sum
bernoulli'_def 📖	mathematical	—	bernoulli' Finset.sum Rat.addCommMonoid Finset.range Nat.choose	—	bernoulli'_def' Fin.sum_univ_eq_sum_range
bernoulli'_def' 📖	mathematical	—	bernoulli' Finset.sum Rat.addCommMonoid Finset.univ Fin.fintype Nat.choose	—	bernoulli'.eq_1
bernoulli'_eq_bernoulli 📖	mathematical	—	bernoulli' bernoulli	—	mul_comm Even.neg_pow Distrib.rightDistribClass Nat.instAtLeastTwoHAddOfNat one_pow one_mul
bernoulli'_eq_zero_of_odd 📖	mathematical	Odd Nat.instSemiring	bernoulli'	—	map_div₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass eq_ratCast map_natCast bernoulli'PowerSeries_mul_exp_sub_one sub_mul mul_sub neg_sub mul_neg neg_eq_iff_eq_neg mul_one map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_sub RingHomClass.toAddMonoidHomClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass mul_assoc mul_comm PowerSeries.exp_mul_exp_neg_eq_one one_mul PowerSeries.evalNegHom_X neg_mul mul_eq_mul_right_iff IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero PowerSeries.instIsDomain Rat.isDomain eq_zero_of_neg_eq Rat.instIsOrderedAddMonoid DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass PowerSeries.coeff_rescale Odd.neg_one_pow sub_neg_eq_add IsStrictOrderedRing.noZeroDivisors Rat.instIsStrictOrderedRing AddGroup.existsAddOfLE Rat.instCharZero PowerSeries.coeff_X neg_zero PowerSeries.coeff_exp zero_add Nat.cast_one div_self Rat.cast_one PowerSeries.coeff_one sub_zero map_zero AddMonoidHomClass.toZeroHomClass NeZero.charZero_one
bernoulli'_four 📖	mathematical	—	bernoulli'	—	bernoulli'_def Finset.sum_congr Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.isNat_ofNat Finset.sum_range_succ Finset.sum_singleton Nat.choose_zero_right Nat.cast_one Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_sub Mathlib.Meta.NormNum.IsNat.to_isInt one_div Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Rat.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat bernoulli'_zero mul_one Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Nat.instAtLeastTwoHAddOfNat Nat.choose_one_right div_self Mathlib.Meta.NormNum.isNat_eq_false Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_zero bernoulli'_one one_mul Mathlib.Meta.NormNum.isNNRat_add Mathlib.Meta.NormNum.IsNNRat.to_isNat bernoulli'_two Nat.choose_succ_self_right bernoulli'_three MulZeroClass.mul_zero add_zero Mathlib.Meta.NormNum.IsRat.neg_to_eq Mathlib.Meta.NormNum.isRat_sub Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.isRat_div Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.isInt_neg
bernoulli'_odd_eq_zero 📖	mathematical	Odd Nat.instSemiring	bernoulli'	—	bernoulli'_eq_zero_of_odd
bernoulli'_one 📖	mathematical	—	bernoulli'	—	bernoulli'_def Finset.sum_congr Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.isNat_ofNat Finset.sum_singleton Nat.choose_succ_self_right Mathlib.Meta.NormNum.isNat_add Nat.cast_one Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_sub Mathlib.Meta.NormNum.IsNat.to_isInt one_div Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Rat.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat bernoulli'_zero mul_one Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_sub Mathlib.Meta.NormNum.IsNNRat.to_isRat
bernoulli'_spec 📖	mathematical	—	Finset.sum Rat.addCommMonoid Finset.range Nat.choose bernoulli'	—	Finset.sum_range_succ_comm bernoulli'_def tsub_self Nat.instCanonicallyOrderedAdd Nat.instOrderedSub Nat.choose_zero_right sub_self zero_add div_one Nat.cast_one one_mul sub_add Finset.sum_sub_distrib sub_eq_zero sub_sub_cancel_left neg_eq_zero Finset.sum_eq_zero Nat.choose_symm le_of_lt Finset.mem_range
bernoulli'_spec' 📖	mathematical	—	Finset.sum Rat.addCommMonoid Finset.HasAntidiagonal.antidiagonal Nat.instAddMonoid Finset.Nat.instHasAntidiagonal Nat.choose bernoulli'	—	Finset.sum_congr add_tsub_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub Finset.mem_range_succ_iff Nat.cast_sub bernoulli'_spec
bernoulli'_three 📖	mathematical	—	bernoulli'	—	bernoulli'_def Finset.sum_congr Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.isNat_ofNat Finset.sum_range_succ Finset.sum_singleton Nat.choose_zero_right Nat.cast_one Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_sub Mathlib.Meta.NormNum.IsNat.to_isInt one_div Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Rat.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat bernoulli'_zero mul_one Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Nat.instAtLeastTwoHAddOfNat Nat.choose_one_right div_self Mathlib.Meta.NormNum.isNat_eq_false Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_zero bernoulli'_one one_mul Mathlib.Meta.NormNum.isNNRat_add Nat.choose_succ_self_right bernoulli'_two Mathlib.Meta.NormNum.IsNNRat.to_isNat sub_self
bernoulli'_two 📖	mathematical	—	bernoulli'	—	bernoulli'_def Finset.sum_congr Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.isNat_ofNat Finset.sum_range_succ Finset.sum_singleton Nat.choose_zero_right Nat.cast_one Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_sub Mathlib.Meta.NormNum.IsNat.to_isInt one_div Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Rat.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat bernoulli'_zero mul_one Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Nat.instAtLeastTwoHAddOfNat Nat.choose_succ_self_right div_self Mathlib.Meta.NormNum.isNat_eq_false Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_zero bernoulli'_one one_mul Mathlib.Meta.NormNum.isNNRat_add Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_sub Mathlib.Meta.NormNum.IsNNRat.to_isRat
bernoulli'_zero 📖	mathematical	—	bernoulli'	—	bernoulli'_def Finset.sum_congr CharP.cast_eq_zero CharP.ofCharZero Rat.instCharZero zero_sub sub_zero
bernoulliPowerSeries_mul_exp_sub_one 📖	mathematical	—	PowerSeries MvPowerSeries.instMul CommSemiring.toSemiring CommRing.toCommSemiring bernoulliPowerSeries SubNegMonoid.toSub AddGroup.toSubNegMonoid PowerSeries.instAddGroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing PowerSeries.exp MvPowerSeries.instOne PowerSeries.X	—	PowerSeries.ext PowerSeries.coeff_zero_eq_constantCoeff map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_sub RingHomClass.toAddMonoidHomClass PowerSeries.constantCoeff_exp sub_self MulZeroClass.mul_zero PowerSeries.coeff_zero_X PowerSeries.coeff_mul Finset.sum_congr DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass PowerSeries.coeff_exp one_div PowerSeries.coeff_one Finset.Nat.sum_antidiagonal_succ' Nat.cast_mul Nat.cast_succ Unique.instSubsingleton sub_zero PowerSeries.coeff_X zero_add bernoulli_one CharP.cast_eq_zero CharP.ofCharZero Rat.instCharZero Nat.cast_one mul_one div_one inv_one map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass Finset.antidiagonal_zero Nat.instCanonicallyOrderedAdd mul_inv_rev Finset.sum_singleton bernoulli_zero div_self NeZero.charZero_one Nat.cast_zero Nat.factorial_ne_zero map_zero MonoidWithZeroHomClass.toZeroHomClass zero_div bernoulli_spec' Finset.sum_div eq_div_of_mul_eq Finset.HasAntidiagonal.mem_antidiagonal Nat.add_choose Nat.cast_div_charZero Nat.factorial_mul_factorial_dvd_factorial_add mul_assoc mul_comm Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.cons_ne_zero ne_of_gt Nat.cast_pos' Rat.instAddLeftMono Rat.instZeroLEOneClass Nat.factorial_pos Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add Nat.cast_nonneg' Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Rat.instIsStrictOrderedRing Rat.nontrivial Mathlib.Meta.NormNum.isNat_ofNat one_ne_zero NeZero.one GroupWithZero.toNontrivial
bernoulli_eq_bernoulli'_of_ne_one 📖	mathematical	—	bernoulli bernoulli'	—	Ne.lt_or_gt bernoulli_zero bernoulli'_zero Nat.even_or_odd bernoulli.eq_1 Even.neg_one_pow one_mul bernoulli'_eq_zero_of_odd bernoulli_eq_zero_of_odd
bernoulli_eq_zero_of_odd 📖	mathematical	Odd Nat.instSemiring	bernoulli	—	bernoulli.eq_1 bernoulli'_eq_zero_of_odd MulZeroClass.mul_zero
bernoulli_one 📖	mathematical	—	bernoulli	—	Mathlib.Meta.NormNum.IsInt.neg_to_eq Mathlib.Meta.NormNum.isInt_pow Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.intPow_negOfNat_bit1 Mathlib.Meta.NormNum.natPow_zero bernoulli'_one Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_inv_pos Rat.instCharZero neg_mul Mathlib.Meta.NormNum.IsRat.neg_to_eq Mathlib.Meta.NormNum.isRat_neg Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.isRat_div Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat
bernoulli_spec' 📖	mathematical	—	Finset.sum Rat.addCommMonoid Finset.HasAntidiagonal.antidiagonal Nat.instAddMonoid Finset.Nat.instHasAntidiagonal Nat.choose bernoulli	—	Finset.sum_congr Finset.antidiagonal_zero Nat.instCanonicallyOrderedAdd Finset.sum_singleton add_zero Nat.choose_self Nat.cast_one CharP.cast_eq_zero CharP.ofCharZero Rat.instCharZero zero_add div_self NeZero.charZero_one bernoulli_zero mul_one add_comm Nat.cast_zero Nat.choose_succ_self_right bernoulli'_spec' Finset.sum_eq_add_sum_diff_singleton add_eq_of_eq_sub' Finset.mem_singleton Finset.mem_sdiff bernoulli_eq_bernoulli'_of_ne_one Finset.antidiagonal_congr Nat.cast_add bernoulli_one zero_sub bernoulli'_one one_div Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul neg_div mul_neg neg_neg Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Meta.NormNum.isNat_eq_false Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_sub Mathlib.Meta.NormNum.IsNat.to_isInt eq_sub_of_add_eq'
bernoulli_two 📖	mathematical	—	bernoulli	—	Even.neg_pow Nat.instAtLeastTwoHAddOfNat one_pow bernoulli'_two one_div one_mul
bernoulli_zero 📖	mathematical	—	bernoulli	—	pow_zero bernoulli'_zero mul_one
sum_Ico_pow 📖	mathematical	—	Finset.sum Rat.addCommMonoid Finset.Ico Nat.instPreorder Nat.instLocallyFiniteOrder Finset.range bernoulli' Nat.choose	—	Nat.cast_succ Finset.sum_congr pow_zero Finset.sum_const Nat.card_Ico add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid nsmul_eq_mul mul_one zero_add Nat.cast_one div_one Finset.sum_singleton bernoulli'_zero Nat.choose_succ_self_right tsub_zero pow_one one_mul Nat.cast_zero Rat.instCharZero mul_div_right_comm mul_div_cancel_right₀ EuclideanDomain.toMulDivCancelClass bernoulli_one Nat.choose_one_right Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_add Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz Mathlib.Tactic.Ring.add_pf_zero_add bernoulli_eq_bernoulli'_of_ne_one Finset.sum_Ico_eq_sub CharP.cast_eq_zero CharP.ofCharZero zero_pow sub_zero Finset.sum_range_succ sum_range_pow Nat.cast_add Finset.sum_range_succ' Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_gt one_div bernoulli_zero Nat.choose_zero_right bernoulli'_one AddRightCancelSemigroup.toIsRightCancelAdd
sum_bernoulli 📖	mathematical	—	Finset.sum Rat.addCommMonoid Finset.range Nat.choose bernoulli	—	Finset.sum_congr zero_add Finset.sum_singleton Nat.choose_succ_self_right Nat.cast_one bernoulli_zero mul_one sum_bernoulli' bernoulli_eq_bernoulli'_of_ne_one Nat.cast_succ Finset.sum_range_succ' Nat.choose_zero_right bernoulli'_zero Nat.choose_one_right bernoulli'_one one_div Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_natCast Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Rat.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.neg_mul Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_add Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf bernoulli_one Nat.cast_zero Mathlib.Tactic.Ring.neg_congr Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Tactic.Ring.add_overlap_pf_zero
sum_bernoulli' 📖	mathematical	—	Finset.sum Rat.addCommMonoid Finset.range Nat.choose bernoulli'	—	CharP.cast_eq_zero CharP.ofCharZero Rat.instCharZero Finset.mul_sum Finset.sum_congr Nat.cast_one Nat.cast_zero Nat.cast_sub LT.lt.le Finset.mem_range Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial mul_comm tsub_add_eq_add_tsub CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Nat.choose_mul_succ_eq Finset.sum_range_succ bernoulli'_def Int.cast_one Int.cast_natCast Nat.choose_succ_self_right Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add
sum_range_pow 📖	mathematical	—	Finset.sum Rat.addCommMonoid Finset.range bernoulli Nat.choose	—	Nat.cast_zero Rat.instCharZero Nat.factorial_ne_zero PowerSeries.ext PowerSeries.coeff_mul Finset.sum_congr Finset.Nat.sum_antidiagonal_eq_sum_range_succ PowerSeries.exp_pow_eq_rescale_exp Nat.instNoMaxOrder Nat.choose_eq_factorial_div_factorial LT.lt.le div_eq_iff mul_assoc mul_comm div_mul_eq_mul_div PowerSeries.coeff_exp one_div map_inv₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_natCast mul_one_div div_div tsub_add_eq_add_tsub CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Nat.cast_div Nat.factorial_mul_factorial_dvd_factorial Nat.cast_mul IsStrictOrderedRing.noZeroDivisors Rat.instIsStrictOrderedRing AddGroup.existsAddOfLE Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Nat.cast_one inv_one PowerSeries.coeff_one sub_zero map_zero AddMonoidHomClass.toZeroHomClass NeZero.charZero_one map_pow MonoidWithZeroHomClass.toMonoidHomClass PowerSeries.constantCoeff_exp one_pow map_one MonoidHomClass.toOneHomClass PowerSeries.sub_const_eq_X_mul_shift mul_right_inj' IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero PowerSeries.instIsDomain Rat.isDomain PowerSeries.exp_pow_sum geom_sum_mul bernoulliPowerSeries_mul_exp_sub_one bernoulliPowerSeries.eq_1 mul_right_comm mul_eq_mul_right_iff IsCancelMulZero.toIsRightCancelMulZero div_eq_mul_inv Finset.sum_mul PowerSeries.ext_iff Nat.cast_add Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero ne_of_gt Nat.cast_pos' Rat.instAddLeftMono Rat.instZeroLEOneClass Nat.factorial_pos Mathlib.Tactic.FieldSimp.NF.cons_ne_zero Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add Nat.cast_nonneg' Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Rat.nontrivial Mathlib.Meta.NormNum.isNat_ofNat one_ne_zero NeZero.one GroupWithZero.toNontrivial

---

← Back to Index