1.1 Prime and p-adic valuation
For a prime \(p\) and a natural number \(m\), \(\operatorname {logn}(p, m)\) is the largest \(k\) such that \(p^k\) divides \(m\). In MathComp this is logn p m.
For \(p \geq 2\) and \(n \in \mathbb {N}\), \(\texttt{trunc\_ log}(p, n)\) is the largest \(k\) such that \(p^k \leq n\).
For prime \(p\) and \(m, n {\gt} 0\),
\[ \operatorname {logn}(p, m \cdot n) = \operatorname {logn}(p, m) + \operatorname {logn}(p, n). \]
For prime \(p\),
\[ \operatorname {logn}(p, p^n) = n. \]
For \(p \geq 2\) and \(n {\gt} 0\),
\[ p^{\texttt{trunc\_ log}(p, n)} \leq n {\lt} p^{\texttt{trunc\_ log}(p, n) + 1}. \]
For \(p \geq 2\) and \(n {\gt} 0\),
\[ n {\lt} p^{\texttt{trunc\_ log}(p, n) + 1}. \]