Theorem sub_one_mul_padicValNat_factorial_eq_sub_sum_digits

Modification history