BernoulliPolynomials

📁 Source: Mathlib/NumberTheory/BernoulliPolynomials.lean

Statistics

Metric	Count
Definitions bernoulli	1
Theorems bernoulli_comp_neg_X, bernoulli_comp_one_add_X, bernoulli_comp_one_sub_X, bernoulli_def, bernoulli_eq_sub_sum, bernoulli_eval_neg, bernoulli_eval_one, bernoulli_eval_one_add, bernoulli_eval_one_sub, bernoulli_eval_zero, bernoulli_generating_function, bernoulli_one, bernoulli_succ_eval, bernoulli_three_eval_one_quarter, bernoulli_zero, coeff_bernoulli, derivative_bernoulli, derivative_bernoulli_add_one, sum_bernoulli, sum_range_pow_eq_bernoulli_sub	20
Total	21

Polynomial

Definitions

Name	Category	Theorems
bernoulli 📖	CompOp	29 math math: bernoulli_eval_one_sub, HurwitzZeta.cosZeta_two_mul_nat', sum_bernoulli, bernoulli_eval_one, HurwitzZeta.cosZeta_two_mul_nat, bernoulli_succ_eval, bernoulli_eval_zero, bernoulli_generating_function, bernoulli_eval_one_add, HurwitzZeta.hurwitzZeta_neg_nat, sum_range_pow_eq_bernoulli_sub, bernoulli_zero, bernoulli_eval_neg, HurwitzZeta.hurwitzZetaOdd_neg_two_mul_nat, hasSum_one_div_nat_pow_mul_cos, bernoulli_eq_sub_sum, HurwitzZeta.hurwitzZetaEven_one_sub_two_mul_nat, HurwitzZeta.sinZeta_two_mul_nat_add_one', bernoulli_comp_one_add_X, bernoulli_def, HurwitzZeta.sinZeta_two_mul_nat_add_one, hasSum_one_div_nat_pow_mul_sin, derivative_bernoulli_add_one, bernoulli_one, coeff_bernoulli, derivative_bernoulli, bernoulli_comp_one_sub_X, bernoulli_comp_neg_X, bernoulli_three_eval_one_quarter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bernoulli_comp_neg_X 📖	mathematical	—	comp Rat.semiring bernoulli Polynomial instNeg DivisionRing.toRing Rat.instDivisionRing X instZSMul Monoid.toNatPow Int.instMonoid instAdd instNSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	—	bernoulli_zero one_comp pow_zero zero_tsub Nat.instCanonicallyOrderedAdd Nat.instOrderedSub zero_nsmul add_zero one_smul ext neg_one_mul C_1 C_neg comp_C_mul_X_coeff coeff_smul coeff_add coeff_bernoulli coeff_X_pow add_tsub_cancel_left IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid bernoulli_one Nat.choose_succ_self_right Nat.cast_add Nat.cast_one nsmul_eq_mul mul_one smul_add zsmul_eq_mul Int.cast_pow Int.cast_neg Int.cast_one Nat.even_or_odd bernoulli_eq_zero_of_odd MulZeroClass.zero_mul nsmul_zero smul_zero
bernoulli_comp_one_add_X 📖	mathematical	—	comp Rat.semiring bernoulli Polynomial instAdd instOne X instNSMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	—	Nat.strong_induction_on bernoulli_zero one_comp zero_tsub Nat.instCanonicallyOrderedAdd Nat.instOrderedSub pow_zero zero_nsmul add_zero IsAddTorsionFree.to_isTorsionFree_nat IsAddTorsionFree.of_isCancelMulZero_charZero charZero Rat.instCharZero instIsCancelMulZeroOfIsCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsStrictOrderedRing.toIsOrderedCancelAddMonoid Rat.instIsStrictOrderedRing IsDomain.toIsCancelMulZero Rat.isDomain Nat.instIsCancelMulZero ne_of_gt Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid zero_le Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat smul_comp IsScalarTower.right smul_add Nat.instAtLeastTwoHAddOfNat bernoulli_eq_sub_sum add_assoc one_add_one_eq_two Finset.sum_congr sub_comp sum_comp smul_smul Finset.mem_range Finset.sum_add_distrib sub_add sub_add_eq_sub_sub_swap sub_sub_eq_add_sub smul_sub X_pow_comp one_add_X_pow_sub_X_pow Finset.smul_sum Nat.add_one_mul_choose_eq Finset.sum_range_succ nsmul_eq_mul Nat.cast_mul Nat.cast_add Nat.cast_one Finset.sum_range_succ' zero_add Nat.choose_one_right CharP.cast_eq_zero charP CharP.ofCharZero mul_one add_tsub_cancel_right IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Nat.choose_zero_right MulZeroClass.mul_zero mul_assoc Nat.choose_succ_self_right
bernoulli_comp_one_sub_X 📖	mathematical	—	comp Rat.semiring bernoulli Polynomial instSub DivisionRing.toRing Rat.instDivisionRing instOne X instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring instNeg	—	bernoulli_zero one_comp pow_zero mul_one sub_eq_add_neg comp_assoc add_comp X_comp bernoulli_comp_one_add_X add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid nsmul_eq_mul Nat.cast_add Nat.cast_one bernoulli_comp_neg_X smul_add zsmul_eq_mul Int.cast_pow Int.cast_neg Int.cast_one mul_comp natCast_comp pow_comp neg_pow add_assoc Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_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.atom_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add 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 Mathlib.Tactic.Ring.cast_zero Nat.cast_zero
bernoulli_def 📖	mathematical	—	bernoulli Finset.sum Polynomial Rat.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing Rat.commRing Finset.range DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring semiring Semiring.toModule module LinearMap.instFunLike monomial bernoulli Nat.choose	—	Finset.sum_range_reflect add_zero bernoulli.eq_1 Finset.sum_congr Nat.choose_symm Finset.mem_range_succ_iff tsub_tsub_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le
bernoulli_eq_sub_sum 📖	mathematical	—	Polynomial Rat.semiring instNSMul bernoulli instSub DivisionRing.toRing Rat.instDivisionRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring X Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing Rat.commRing Finset.range Nat.choose	—	Nat.cast_smul_eq_nsmul Finset.sum_congr smul_X_eq_monomial Nat.cast_succ sum_bernoulli Finset.sum_range_succ_sub_sum Nat.choose_succ_self_right
bernoulli_eval_neg 📖	mathematical	—	eval Rat.semiring bernoulli	—	mul_add Distrib.leftDistribClass eval_comp eval_neg eval_X nsmul_eq_mul smul_add zsmul_eq_mul Int.cast_pow Int.cast_neg Int.cast_one eval_add eval_mul eval_pow eval_one eval_natCast bernoulli_comp_neg_X
bernoulli_eval_one 📖	mathematical	—	eval Rat.semiring bernoulli bernoulli'	—	eval_finset_sum Finset.sum_congr eval_monomial one_pow mul_one Finset.sum_range_succ sum_bernoulli Nat.choose_self Nat.cast_one one_mul bernoulli_one Mathlib.Meta.NormNum.IsRat.neg_to_eq Mathlib.Meta.NormNum.isRat_div Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.isNNRat_inv_pos Rat.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_add Mathlib.Meta.NormNum.isRat_neg Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul bernoulli'_one bernoulli_eq_bernoulli'_of_ne_one zero_add
bernoulli_eval_one_add 📖	mathematical	—	eval Rat.semiring bernoulli	—	bernoulli_comp_one_add_X eval_comp eval_add eval_one eval_X nsmul_eq_mul eval_mul eval_natCast eval_pow
bernoulli_eval_one_sub 📖	mathematical	—	eval Rat.semiring bernoulli	—	eval_comp eval_sub eval_one eval_X eval_mul eval_pow eval_neg bernoulli_comp_one_sub_X
bernoulli_eval_zero 📖	mathematical	—	eval Rat.semiring bernoulli bernoulli	—	bernoulli.eq_1 eval_finset_sum Finset.sum_range_succ Finset.sum_eq_zero zero_pow Nat.instCanonicallyOrderedAdd Nat.instOrderedSub Finset.mem_range MulZeroClass.mul_zero Finset.sum_congr eval_monomial tsub_self Nat.choose_self Nat.cast_one mul_one eval_C zero_add
bernoulli_generating_function 📖	mathematical	—	PowerSeries MvPowerSeries.instMul CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe AlgHom Polynomial Rat.commSemiring semiring algebraOfAlgebra Algebra.id AlgHom.funLike aeval Rat.semiring Algebra.toSMul Nat.factorial bernoulli SubNegMonoid.toSub AddGroup.toSubNegMonoid PowerSeries.instAddGroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing PowerSeries.exp MvPowerSeries.instOne PowerSeries.X RingHom Semiring.toNonAssocSemiring PowerSeries.instSemiring RingHom.instFunLike PowerSeries.rescale	—	PowerSeries.ext one_div map_smul SemilinearMapClass.toMulActionSemiHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass PowerSeries.coeff_zero_eq_constantCoeff map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Nat.cast_one inv_one bernoulli_zero map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass one_smul map_sub RingHomClass.toAddMonoidHomClass PowerSeries.constantCoeff_exp sub_self MulZeroClass.mul_zero PowerSeries.constantCoeff_X MulZeroClass.zero_mul PowerSeries.coeff_succ_X_mul PowerSeries.coeff_rescale PowerSeries.coeff_exp PowerSeries.coeff_mul Finset.sum_range_succ Finset.sum_congr DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass tsub_self Nat.instCanonicallyOrderedAdd Nat.instOrderedSub add_zero Nat.cast_zero Rat.instCharZero Nat.factorial_ne_zero IsUnit.map mul_left_comm Nat.cast_mul mul_assoc mul_one_div_cancel Nat.cast_ne_zero mul_one mul_comm aeval_monomial Nat.cast_add sum_bernoulli Finset.mul_sum map_sum NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass Algebra.smul_def aeval_mul aeval_C PowerSeries.coeff_one Finset.mem_range_sub_ne_zero sub_zero mul_right_comm Nat.cast_choose Finset.mem_range_le Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons one_mul Mathlib.Tactic.FieldSimp.zpow'_one
bernoulli_one 📖	mathematical	—	bernoulli Polynomial Rat.semiring instSub DivisionRing.toRing Rat.instDivisionRing X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C	—	Finset.sum_congr Finset.sum_range_succ Finset.sum_singleton bernoulli_zero Nat.choose_succ_self_right zero_add Nat.cast_one mul_one tsub_zero Nat.instOrderedSub pow_one one_smul bernoulli_one neg_div one_div Nat.choose_self tsub_self Nat.instCanonicallyOrderedAdd pow_zero neg_smul smul_C sub_eq_add_neg
bernoulli_succ_eval 📖	mathematical	—	eval Rat.semiring bernoulli bernoulli Finset.sum Rat.addCommMonoid Finset.range	—	eq_add_of_sub_eq' sum_range_pow_eq_bernoulli_sub
bernoulli_three_eval_one_quarter 📖	mathematical	—	eval Rat.semiring bernoulli	—	Finset.sum_range_succ eval_add eval_monomial Finset.sum_range_zero eval_zero zero_add bernoulli_one bernoulli_eq_bernoulli'_of_ne_one zero_ne_one bernoulli'_zero bernoulli'_two bernoulli'_three Nat.choose_zero_right Nat.cast_one mul_one Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_pow Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isNNRat_inv_pos Rat.instCharZero Mathlib.Meta.NormNum.isNat_natSub Mathlib.Meta.NormNum.one_natPow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit1 one_mul Nat.instAtLeastTwoHAddOfNat Mathlib.Meta.NormNum.IsRat.neg_to_eq Mathlib.Meta.NormNum.isRat_div Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNNRat.to_isRat Nat.choose_one_right neg_mul Mathlib.Meta.NormNum.isRat_neg Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Meta.NormNum.isRat_add Nat.choose_succ_self_right Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.natPow_one Mathlib.Meta.NormNum.IsRat.to_isNNRat Nat.choose_self Mathlib.Meta.NormNum.natPow_zero MulZeroClass.zero_mul add_zero
bernoulli_zero 📖	mathematical	—	bernoulli Polynomial Rat.semiring instOne	—	Finset.sum_congr zero_add zero_tsub Nat.instCanonicallyOrderedAdd Nat.instOrderedSub map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_natCast Finset.sum_singleton bernoulli_zero map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass Nat.choose_self Nat.cast_one mul_one
coeff_bernoulli 📖	mathematical	—	coeff Rat.semiring bernoulli bernoulli Nat.choose	—	finset_sum_coeff Finset.sum_congr coeff_monomial Finset.sum_ite_eq_of_mem Finset.sum_eq_zero
derivative_bernoulli 📖	mathematical	—	DFunLike.coe LinearMap Rat.semiring RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative bernoulli instMul instNatCast	—	Nat.cast_zero MulZeroClass.zero_mul bernoulli_zero derivative_one Nat.cast_one derivative_bernoulli_add_one
derivative_bernoulli_add_one 📖	mathematical	—	DFunLike.coe LinearMap Rat.semiring RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative bernoulli instMul instAdd instNatCast instOne	—	derivative_sum Finset.sum_congr derivative_monomial Finset.range_add_one Finset.sum_insert Finset.notMem_range_self tsub_self Nat.instCanonicallyOrderedAdd Nat.instOrderedSub Nat.cast_zero MulZeroClass.mul_zero map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass zero_add Finset.mul_sum Nat.cast_one Nat.cast_add C_eq_natCast C_mul_monomial mul_comm mul_assoc Nat.cast_mul Nat.choose_mul_succ_eq
sum_bernoulli 📖	mathematical	—	Finset.sum Polynomial Rat.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing Rat.commRing Finset.range Algebra.toSMul Rat.commSemiring semiring algebraOfAlgebra Algebra.id Nat.choose bernoulli DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule module LinearMap.instFunLike monomial	—	Finset.sum_congr bernoulli_def Finset.smul_sum Finset.range_eq_Ico Finset.sum_Ico_eq_sum_range tsub_zero Nat.instOrderedSub zero_add add_tsub_cancel_left IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass smul_monomial mul_comm Nat.cast_mul Nat.choose_mul mul_assoc smul_eq_mul Finset.sum_range_succ_comm Finset.sum_singleton Nat.choose_succ_self_right Nat.cast_one bernoulli_zero mul_one Nat.cast_add one_smul Finset.sum_eq_zero sum_bernoulli NeZero.charZero_one Rat.instCharZero zero_smul
sum_range_pow_eq_bernoulli_sub 📖	mathematical	—	Finset.sum Rat.addCommMonoid Finset.range eval Rat.semiring bernoulli bernoulli	—	sum_range_pow bernoulli_def eval_finset_sum Finset.sum_div mul_div_cancel₀ Nat.cast_one Nat.cast_zero Rat.instCharZero Finset.sum_congr eval_monomial Finset.sum_flip Finset.sum_range_succ tsub_self Nat.instCanonicallyOrderedAdd Nat.instOrderedSub tsub_zero Nat.choose_zero_right mul_one pow_zero add_tsub_cancel_right AddGroup.toOrderedSub covariant_swap_add_of_covariant_add Rat.instAddLeftMono IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Finset.mem_range_le Nat.choose_symm

---

← Back to Index