Lucas

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

Statistics

Metric	Count
Definitions	0
Theorems choose_modEq_choose_mod_mul_choose_div, choose_modEq_choose_mod_mul_choose_div_nat, choose_modEq_choose_mul_prod_range_choose, choose_modEq_prod_range_choose, choose_modEq_prod_range_choose_nat, choose_mul_mul_modEq_choose, choose_mul_mul_modEq_choose_nat, choose_pow_mul_pow_mul_modEq_choose, choose_pow_mul_pow_mul_modEq_choose_nat, lucas_theorem, lucas_theorem_nat	11
Total	11

Choose

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
choose_modEq_choose_mod_mul_choose_div 📖	mathematical	—	Int.ModEq Nat.choose	—	one_pow add_pow_eq_mul_pow_add_pow_div_char Polynomial.instCharP ZMod.charP Polynomial.coeff_X_add_one_pow eq_intCast RingHom.instRingHomClass Polynomial.map_pow Polynomial.map_add Polynomial.map_X Polynomial.map_one add_pow Finset.sum_congr mul_one Finset.sum_mul_sum mul_assoc mul_right_comm pow_add Nat.cast_mul lt_of_lt_of_le NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' right_eq_add instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Polynomial.finset_sum_coeff Polynomial.coeff_mul_natCast Polynomial.coeff_X_pow ite_mul MulZeroClass.zero_mul Finset.sum_product' if_congr Finset.sum_ite_eq one_mul Int.cast_mul Int.cast_natCast not_lt not_le not_and_or Finset.mem_range Finset.mem_product Nat.choose_eq_zero_of_lt CharP.cast_eq_zero CharP.ofCharZero Int.instCharZero Int.cast_zero MulZeroClass.mul_zero
choose_modEq_choose_mod_mul_choose_div_nat 📖	mathematical	—	Nat.ModEq Nat.choose	—	Int.natCast_modEq_iff choose_modEq_choose_mod_mul_choose_div
choose_modEq_choose_mul_prod_range_choose 📖	mathematical	—	Int.ModEq Nat.choose Monoid.toPow Nat.instMonoid Finset.prod Nat.instCommMonoid Finset.range	—	pow_zero Nat.cast_one mul_one Int.ModEq.trans Finset.prod_range_succ Nat.cast_mul mul_assoc mul_right_comm Int.ModEq.mul choose_modEq_choose_mod_mul_choose_div pow_succ mul_comm Int.ModEq.refl
choose_modEq_prod_range_choose 📖	mathematical	Monoid.toPow Nat.instMonoid	Int.ModEq Nat.choose Finset.prod Int.instCommMonoid Finset.range Monoid.toPow Nat.instMonoid	—	Int.ModEq.trans choose_modEq_choose_mul_prod_range_choose Nat.cast_one one_mul Nat.cast_prod
choose_modEq_prod_range_choose_nat 📖	mathematical	Monoid.toPow Nat.instMonoid	Nat.ModEq Nat.choose Finset.prod Nat.instCommMonoid Finset.range Monoid.toPow Nat.instMonoid	—	Int.natCast_modEq_iff choose_modEq_prod_range_choose
choose_mul_mul_modEq_choose 📖	mathematical	—	Int.ModEq Nat.choose	—	Mathlib.Tactic.GCongr.rel_imp_rel Int.ModEq.instIsTrans choose_modEq_choose_mod_mul_choose_div Int.ModEq.refl Nat.choose_self Nat.cast_one Nat.instCanonicallyOrderedAdd NeZero.of_gt' Nat.Prime.one_lt' one_mul
choose_mul_mul_modEq_choose_nat 📖	mathematical	—	Nat.ModEq Nat.choose	—	Int.natCast_modEq_iff choose_mul_mul_modEq_choose
choose_pow_mul_pow_mul_modEq_choose 📖	mathematical	—	Int.ModEq Nat.choose Monoid.toPow Nat.instMonoid	—	pow_zero one_mul mul_assoc Mathlib.Tactic.GCongr.rel_imp_rel Int.ModEq.instIsTrans choose_mul_mul_modEq_choose Int.ModEq.refl
choose_pow_mul_pow_mul_modEq_choose_nat 📖	mathematical	—	Nat.ModEq Nat.choose Monoid.toPow Nat.instMonoid	—	Int.natCast_modEq_iff choose_pow_mul_pow_mul_modEq_choose
lucas_theorem 📖	mathematical	Monoid.toPow Nat.instMonoid	Int.ModEq Nat.choose Finset.prod Int.instCommMonoid Finset.range Monoid.toPow Nat.instMonoid	—	choose_modEq_prod_range_choose
lucas_theorem_nat 📖	mathematical	Monoid.toPow Nat.instMonoid	Nat.ModEq Nat.choose Finset.prod Nat.instCommMonoid Finset.range Monoid.toPow Nat.instMonoid	—	choose_modEq_prod_range_choose_nat

---

← Back to Index