Sylvester-Schur: p-adic valuation

Stream: Is there code for X?

[J. J. Issai (project started by GRP)]

over in #new members > Working on a project: Sylvester-Schur I have started a query. I am interested in code for Legendre's formula for the exact power of a prime p dividing factorial n, namely $\nu_p(n!) = \sum_{e>0} \lfloor n/p^e \rfloor$ . Can someone help me find this in Mathlib?

I would also like to see how this is used in Lean proofs, so that I can prove (or find in Mathlib) two other items referenced in the new members thread: Law of Ademption and Fundamental Inequality.
GRP 2025.06.20.

[Jz Pan]

Nat.Prime.emultiplicity_factorial or Nat.Prime.pow_dvd_factorial_iff or padicValNat_factorial

It's unfortunate that $\nu_p$ has several spellings in mathlib.

[J. J. Issai (project started by GRP)]

Jz Pan: Thanks! I'll go check those out. GRP 2025.06.20.

[J. J. Issai (project started by GRP)]

@Jz Pan Thanks again. (Still learning Zulip interface.)