Commit 2023-09-03 14:49 8c7f8f7d

View on Github →

feat(NumberTheory/Padics/PadicVal): factorial_choose' (#5860)

depends on: #5803

Estimated changes

Modified Mathlib/Data/Nat/Multiplicity.lean

added theorem Nat.Prime.multiplicity_choose'

Modified Mathlib/NumberTheory/Padics/PadicVal.lean

added theorem padicValNat_choose'

added theorem sub_one_mul_padicValNat_choose_eq_sub_sum_digits'

added theorem sub_one_mul_padicValNat_choose_eq_sub_sum_digits