Commit 2023-08-12 17:00 4fbcc51d

View on Github →

feat(NumberTheory/Padics/PadicVal): padicValNat_factorial' (#5803)

depends on: #5778
depends on: #5789
depends on: #5802
depends on: #6505

Estimated changes

Modified Mathlib/Data/Nat/Multiplicity.lean

Modified Mathlib/NumberTheory/Padics/PadicVal.lean

modified theorem padicValNat_choose

modified theorem padicValNat_eq_zero_of_mem_Ioo

modified theorem padicValNat_factorial

modified theorem padicValNat_factorial_mul

modified theorem padicValNat_factorial_mul_add

modified theorem padicValNat_mul_div_factorial

added theorem sub_one_mul_padicValNat_factorial_eq_sub_sum_digits