Central

📁 Source: Mathlib/Data/Nat/Choose/Central.lean

Statistics

Metric	Count
Definitions centralBinom	1
Theorems centralBinom_eq_two_mul_choose, centralBinom_ne_zero, centralBinom_pos, centralBinom_zero, choose_le_centralBinom, four_pow_le_two_mul_self_mul_centralBinom, four_pow_lt_mul_centralBinom, succ_dvd_centralBinom, succ_mul_centralBinom_succ, two_dvd_centralBinom_of_one_le, two_dvd_centralBinom_succ, two_le_centralBinom	12
Total	13

Nat

Definitions

Name	Category	Theorems
centralBinom 📖	CompOp	18 math math: succ_mul_catalan_eq_centralBinom, four_pow_le_two_mul_self_mul_centralBinom, two_dvd_centralBinom_of_one_le, succ_dvd_centralBinom, factorization_centralBinom_eq_zero_of_two_mul_lt, four_pow_lt_mul_centralBinom, centralBinom_pos, factorization_centralBinom_of_two_mul_self_lt_three_mul, centralBinom_eq_two_mul_choose, two_le_centralBinom, centralBinom_factorization_small, centralBinom_zero, prod_pow_factorization_centralBinom, two_dvd_centralBinom_succ, succ_mul_centralBinom_succ, centralBinom_le_of_no_bertrand_prime, catalan_eq_centralBinom_div, choose_le_centralBinom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
centralBinom_eq_two_mul_choose 📖	mathematical	—	centralBinom choose	—	—
centralBinom_ne_zero 📖	—	—	—	—	LT.lt.ne' centralBinom_pos
centralBinom_pos 📖	mathematical	—	centralBinom	—	choose_pos zero_lt_two instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid
centralBinom_zero 📖	mathematical	—	centralBinom	—	choose_zero_right
choose_le_centralBinom 📖	mathematical	—	choose centralBinom	—	choose_le_middle instAtLeastTwoHAddOfNat zero_lt_two instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid
four_pow_le_two_mul_self_mul_centralBinom 📖	mathematical	—	Monoid.toNatPow instMonoid centralBinom	—	pow_one mul_one add_zero LT.lt.le four_pow_lt_mul_centralBinom le_add_self instCanonicallyOrderedAdd mul_assoc zero_lt_two instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid
four_pow_lt_mul_centralBinom 📖	mathematical	—	Monoid.toNatPow instMonoid centralBinom	—	strong_induction_on lt_trichotomy not_lt Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0 add_zero Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.isNat_lt_true IsStrictOrderedRing.toIsOrderedRing instIsStrictOrderedRing instCharZero mul_lt_mul_of_pos_left LinearOrderedCommMonoidWithZero.toPosMulStrictMono Mathlib.Meta.Positivity.pos_of_isNat instNontrivial mul_assoc le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos 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.mul_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Tactic.Ring.mul_pf_left 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.Linarith.add_lt_of_neg_of_le Int.instIsStrictOrderedRing neg_neg_of_pos Int.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Tactic.Linarith.natCast_nonneg Int.instCharZero cast_mul cast_add cast_one succ_mul_centralBinom_succ
succ_dvd_centralBinom 📖	mathematical	—	centralBinom	—	instAtLeastTwoHAddOfNat two_mul add_assoc coprime_add_self_right coprime_self_add_left zero_lt_two instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid mul_assoc succ_mul_centralBinom_succ mul_comm mul_dvd_mul_left two_dvd_centralBinom_succ
succ_mul_centralBinom_succ 📖	mathematical	—	centralBinom	—	mul_comm choose_succ_right_eq choose_mul_succ_eq Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add instAtLeastTwoHAddOfNat two_mul add_assoc mul_assoc
two_dvd_centralBinom_of_one_le 📖	mathematical	—	centralBinom	—	two_dvd_centralBinom_succ
two_dvd_centralBinom_succ 📖	mathematical	—	centralBinom	—	centralBinom_eq_two_mul_choose instAtLeastTwoHAddOfNat two_mul add_assoc choose_succ_succ' choose_symm_add
two_le_centralBinom 📖	mathematical	—	centralBinom	—	choose_one_right choose_le_centralBinom

---

← Back to Index