Commit 2023-07-20 12:44 a1451be4

View on Github →

feat(NumberTheory/Padics/PadicVal): lemmas with factorial (#5789)

Estimated changes

Modified Mathlib/NumberTheory/Padics/PadicVal.lean

added theorem padicValNat_eq_zero_of_mem_Ioo

modified theorem padicValNat_factorial_mul

added theorem padicValNat_factorial_mul_add

added theorem padicValNat_mul_div_factorial