Commit 2023-03-29 02:11 db524829

View on Github →

feat: port Data.Nat.Choose.Factorization (#3158)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/Choose/Factorization.lean

added theorem Nat.factorization_centralBinom_eq_zero_of_two_mul_lt

added theorem Nat.factorization_centralBinom_of_two_mul_self_lt_three_mul

added theorem Nat.factorization_choose_eq_zero_of_lt

added theorem Nat.factorization_choose_le_log

added theorem Nat.factorization_choose_le_one

added theorem Nat.factorization_choose_of_lt_three_mul

added theorem Nat.factorization_factorial_eq_zero_of_lt

added theorem Nat.le_two_mul_of_factorization_centralBinom_pos

added theorem Nat.pow_factorization_choose_le

added theorem Nat.prod_pow_factorization_centralBinom

added theorem Nat.prod_pow_factorization_choose