padicValNat_factorial: another version of Legendre's theorem

Stream: Is there code for X?

[Moritz Firsching]

continued from https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/get.20the.20lastDrop

Using a slighly different path, I got padicValNat_factorial.

Which of

• digits_monotone,
• digit_sum_le,
• padicValNat_factorial_mul,
• padicValNat_add_eq_self_of_lt,
• padicValNat_factorial_add
• padicValNat_factorial_div (possibly with better names), which I use in the proof of padicValNat_factorial might be a good addition to mathlib?

When we have padicValNat_factorial, Kummer's theorem should be quite easy too.

import Mathlib.Tactic
import Mathlib.Data.Nat.Digits
open Nat

theorem digits_monotone {p q : ℕ} (L : List ℕ) (h : p ≤ q) : ofDigits p L ≤ ofDigits q L := by
  induction' L with _ _ hi
  · rfl
  · simp only [ofDigits, cast_id, add_le_add_iff_left]
    exact Nat.mul_le_mul h hi

theorem digit_sum_le (p n : ℕ) (hp : 1 ≤ p) : List.sum (digits p n) ≤ n  := by
  nth_rw 2 [← ofDigits_digits p n]
  rw [← ofDigits_one <| digits p n]
  exact digits_monotone (digits p n) hp

theorem padicValNat_factorial_mul {p : ℕ} (n : ℕ) (hp : p.Prime):
    padicValNat p ((p * n) !) =  padicValNat p (n !)  + n :=  by
  refine' PartENat.natCast_inj.mp _
  rw [padicValNat_def' (Nat.Prime.ne_one hp) <| factorial_pos (p * n)]
  push_cast
  rw [padicValNat_def' (Nat.Prime.ne_one hp) <| factorial_pos n]
  exact @Nat.Prime.multiplicity_factorial_mul n p hp

theorem padicValNat_add_eq_self_of_lt {p m : ℕ} (n : ℕ) (hn : 0 < m) (hm : m < p):
    padicValNat p (p * n + m) = 0 := by
    refine' padicValNat.eq_zero_of_not_dvd <|
        @not_dvd_of_between_consec_multiples _ p n (Nat.lt_add_of_pos_right hn) _
    rw [mul_add, mul_one]
    exact Nat.add_lt_add_left hm (p * n)

theorem padicValNat_factorial_add {p n : ℕ} (m : ℕ) (hp : p.Prime) (h : n < p):
    padicValNat p (p * m + n) ! = padicValNat p (p * m) ! := by
  induction' n with n hn
  · rw [zero_eq, add_zero]
  · rw [add_succ, factorial_succ, @padicValNat.mul _ _ _ { out := hp } (succ_ne_zero (p * m + n))
        <| factorial_ne_zero (p * m + _), hn <| lt_of_succ_lt h, ←add_succ,
        padicValNat_add_eq_self_of_lt _ (succ_pos _) h, zero_add]

theorem padicValNat_factorial_div {p : ℕ} (n : ℕ)  (hp : p.Prime):
   padicValNat p n ! = padicValNat p (p * (n / p))! := by
  nth_rw 1 [← div_add_mod n p]
  exact padicValNat_factorial_add (n / p) hp <| mod_lt n <|Prime.pos hp

theorem padicValNat_factorial {p : ℕ} (hp : p.Prime) (n : ℕ):
    (p - 1) * ((padicValNat p (n !)) : ℕ ) = (n - (p.digits n).sum) := by
  apply Nat.strongInductionOn n
  intro n hn
  by_cases n = 0
  · simp only [h, ge_iff_le, factorial, padicValNat.one, mul_zero, ne_eq, digits_zero, List.sum_nil,
        le_refl, tsub_eq_zero_of_le]
  · suffices padicValNat p (n !) = n / p + padicValNat p ((n/p)!) by
      rw [this, mul_add, hn (n / p) (Nat.div_lt_self (Nat.pos_of_ne_zero h) (Prime.one_lt hp))]
      suffices (p.digits n).sum = n % p + (digits p (n / p)).sum by
        nth_rw 4 [← div_add_mod' n p]
        rw [this, sub_add_eq, Nat.add_sub_cancel, Nat.mul_sub_right_distrib p 1 _, one_mul,
          ← Nat.add_sub_assoc (digit_sum_le p (n / p) (Prime.pos hp)) _,
          Nat.sub_add_cancel <| le_mul_of_pos_left (Prime.pos hp), mul_comm]
      rw [digits_def' (Nat.Prime.one_lt hp) (Nat.pos_of_ne_zero h)]
      exact List.foldl_assoc_comm_cons
    rw [add_comm, ← padicValNat_factorial_mul (n / p) hp]
    exact padicValNat_factorial_div n hp

[Moritz Firsching]

This is now pr-ed: https://github.com/leanprover-community/mathlib4/pull/5803
Reviews welcome!