Lean-Workbook Plus 63770: Prime multiplicity of a prime-power binomial coefficient

If $p$ is prime and $t$ is a positive integer, then the multiplicity of $p$ in $\binom{p^t}{p^{t-1}}$ is exactly $1$.

Source: Lean-Workbook row lean_workbook_plus_63770 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.