Factorization

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

Statistics

Metric	Count
Definitions	0
Theorems factorization_centralBinom_eq_zero_of_two_mul_lt, factorization_centralBinom_of_two_mul_self_lt_three_mul, factorization_choose, factorization_choose', factorization_choose_eq_zero_of_lt, factorization_choose_le_log, factorization_choose_le_one, factorization_choose_of_lt_three_mul, factorization_choose_prime_pow, factorization_choose_prime_pow_add_factorization, factorization_factorial, factorization_factorial_eq_zero_of_lt, factorization_factorial_le_div_pred, factorization_factorial_mul, factorization_factorial_mul_succ, factorization_le_factorization_choose_add, factorization_le_factorization_of_dvd_right, le_two_mul_of_factorization_centralBinom_pos, multiplicity_choose_aux, pow_factorization_choose_le, prod_pow_factorization_centralBinom, prod_pow_factorization_choose, sub_one_mul_factorization_factorial	23
Total	23

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
factorization_centralBinom_eq_zero_of_two_mul_lt 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization centralBinom	—	factorization_choose_eq_zero_of_lt
factorization_centralBinom_of_two_mul_self_lt_three_mul 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization centralBinom	—	factorization_choose_of_lt_three_mul LE.le.trans instAtLeastTwoHAddOfNat two_mul add_tsub_cancel_left instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid le_refl
factorization_choose 📖	mathematical	Prime log	DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization choose Finset.card Finset.filter Monoid.toNatPow instMonoid Finset.Ico instPreorder instLocallyFiniteOrder	—	factorization_choose'
factorization_choose' 📖	mathematical	Prime log	DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization choose Finset.card Finset.filter Monoid.toNatPow instMonoid Finset.Ico instPreorder instLocallyFiniteOrder	—	choose_mul_factorial_mul_factorial add_tsub_cancel_right instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid Pi.add_apply Finsupp.coe_add factorization_mul choose_pos ne_of_gt mul_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono factorial_pos mul_assoc factorization_factorial factorial_ne_zero LE.le.trans_lt log_mono_right add_comm multiplicity_choose_aux Finset.sum_congr Finset.filter.congr_simp
factorization_choose_eq_zero_of_lt 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization choose	—	choose_eq_zero_of_lt factorization_zero choose_eq_factorial_div_factorial instCanonicallyOrderedAdd instOrderedSub factorization_div factorial_mul_factorial_dvd_factorial Finsupp.coe_tsub Pi.sub_apply factorization_factorial_eq_zero_of_lt zero_tsub
factorization_choose_le_log 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization choose log	—	instCanonicallyOrderedAdd Not.imp_symm factorization_eq_zero_of_not_prime le_of_not_gt choose_eq_zero_of_lt factorization_zero factorization_choose LE.le.trans_eq Finset.card_filter_le card_Ico
factorization_choose_le_one 📖	mathematical	Monoid.toNatPow instMonoid	DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization choose	—	LE.le.trans factorization_choose_le_log eq_or_ne log_zero_right instCanonicallyOrderedAdd log_lt_of_lt_pow
factorization_choose_of_lt_three_mul 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization choose	—	em' factorization_eq_zero_of_not_prime lt_or_ge choose_eq_zero_of_lt factorization_zero factorization_choose eq_or_lt_of_le pow_one add_lt_add_iff_left IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid contravariant_lt_of_covariant_le instAtLeastTwoHAddOfNat two_mul add_add_add_comm lt_of_le_of_lt add_le_add_left covariant_swap_add_of_covariant_add le_mul_of_one_le_right' instMulLeftMono Prime.pos add_tsub_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE instCanonicallyOrderedAdd instOrderedSub lt_of_le_of_ne Prime.two_le mul_le_mul_left covariant_swap_mul_of_covariant_mul sq pow_right_mono₀ instZeroLEOneClass IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing instIsStrictOrderedRing LT.lt.le Prime.one_lt tsub_le_self
factorization_choose_prime_pow 📖	mathematical	Prime Monoid.toNatPow instMonoid	DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization choose	—	factorization_choose_prime_pow_add_factorization
factorization_choose_prime_pow_add_factorization 📖	mathematical	Prime Monoid.toNatPow instMonoid	DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization choose	—	le_antisymm Finset.filter.congr_simp instNoMaxOrder zero_add pow_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono instZeroLEOneClass Prime.pos factorization_choose factorization_eq_card_pow_dvd_of_lt Ne.bot_lt lt_of_le_of_lt Prime.one_lt log_pow Finset.card_union_of_disjoint Finset.filter_union_right Finset.card_filter_le card_Ico factorization_pow_self factorization_le_factorization_choose_add
factorization_factorial 📖	mathematical	Prime log	DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization factorial Finset.sum instAddCommMonoid Finset.Ico instPreorder instLocallyFiniteOrder Monoid.toNatPow instMonoid	—	factorization_one Finset.sum_congr Finset.sum_const_zero factorial_succ factorization_mul factorial_ne_zero Finsupp.coe_add Pi.add_apply LE.le.trans_lt log_mono_right AddRightCancelSemigroup.toIsRightCancelAdd factorization_eq_card_pow_dvd_of_lt lt_pow_of_log_lt Prime.one_lt Finset.sum_add_distrib Finset.sum_boole
factorization_factorial_eq_zero_of_lt 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization factorial	—	factorization_one factorial_succ factorization_mul factorial_ne_zero Finsupp.coe_add Pi.add_apply add_zero factorization_eq_zero_of_lt
factorization_factorial_le_div_pred 📖	mathematical	Prime	DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization factorial	—	factorization_factorial geom_sum_Ico_le Prime.two_le
factorization_factorial_mul 📖	mathematical	Prime	DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization factorial	—	MulZeroClass.mul_zero factorization_one add_zero factorization_factorial_mul_succ factorization_mul factorial_ne_zero Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero
factorization_factorial_mul_succ 📖	mathematical	Prime	DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization factorial	—	Prime.two_le le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.neg_congr 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.add_mul Mathlib.Tactic.Ring.mul_add 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.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Int.instIsStrictOrderedRing Mathlib.Tactic.Linarith.mul_neg neg_neg_of_pos Int.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Meta.NormNum.isNat_lt_true IsStrictOrderedRing.toIsOrderedRing Int.instCharZero Mathlib.Tactic.Linarith.sub_nonpos_of_le cast_mul cast_add cast_one factorization_eq_zero_of_not_dvd Finset.mem_Ico Finset.prod_Ico_id_eq_factorial factorization_prod_apply ne_zero_of_lt Finset.sum_Ico_consecutive add_assoc Finset.sum_Ico_succ_top factorization_mul Finsupp.coe_add Pi.add_apply Prime.factorization_self Finset.sum_congr Finset.sum_const_zero zero_add add_comm
factorization_le_factorization_choose_add 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization choose	—	factorization_zero zero_add instCanonicallyOrderedAdd Pi.add_apply Finsupp.coe_add factorization_mul choose_pos factorization_le_factorization_of_dvd_right add_one_mul_choose_eq dvd_mul_right ne_of_gt Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid zero_le Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing instIsStrictOrderedRing instNontrivial Mathlib.Meta.NormNum.isNat_ofNat
factorization_le_factorization_of_dvd_right 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization	—	factorization_mul IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le instCanonicallyOrderedAdd
le_two_mul_of_factorization_centralBinom_pos 📖	—	DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization centralBinom	—	—	le_of_not_gt pos_iff_ne_zero instCanonicallyOrderedAdd factorization_centralBinom_eq_zero_of_two_mul_lt
multiplicity_choose_aux 📖	mathematical	Prime	Finset.sum instAddCommMonoid Finset.Ico instPreorder instLocallyFiniteOrder Monoid.toNatPow instMonoid Finset.card Finset.filter	—	Finset.sum_congr add_tsub_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid instOrderedSub pow_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono instZeroLEOneClass Prime.pos Finset.sum_add_distrib Finset.sum_boole
pow_factorization_choose_le 📖	mathematical	—	Monoid.toNatPow instMonoid DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization choose	—	pow_le_of_le_log LT.lt.ne' factorization_choose_le_log
prod_pow_factorization_centralBinom 📖	mathematical	—	Finset.prod instCommMonoid Finset.range Monoid.toNatPow instMonoid DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization centralBinom	—	prod_pow_factorization_choose
prod_pow_factorization_choose 📖	mathematical	—	Finset.prod instCommMonoid Finset.range Monoid.toNatPow instMonoid DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization choose	—	factorization_prod_pow_eq_self choose_ne_zero Finset.prod_subset Finset.mem_range Mathlib.Tactic.Contrapose.contrapose₁ Finsupp.mem_support_iff factorization_choose_eq_zero_of_lt pow_zero
sub_one_mul_factorization_factorial 📖	mathematical	Prime	DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization factorial digits	—	factorization_factorial Finset.sum_Ico_add' instIsOrderedCancelAddMonoid CanonicallyOrderedAdd.toExistsAddOfLE instCanonicallyOrderedAdd Finset.sum_congr Ico_zero_eq_range

---

← Back to Index