English
The p-adic valuation on PadicSeq p lifts the p-adic valuation from the stationary point, defined as 0 if f ≈ 0, otherwise the valuation of f at the stationary point.
Русский
Оценка p-падиковой последовательности PadicSeq p поднимается из оценки стационарной точки: она равна 0, если f ≈ 0; иначе — значение оценки в стационарной точке.
LaTeX
$$$\mathrm{valuation}(f) = \begin{cases}0, & f \approx 0 \\ \mathrm{padicVal}_p(f(\mathrm{stationaryPoint}(hf))), & \text{иначе} \end{cases}$$$
Lean4
/-- The `p`-adic valuation on `ℚ` lifts to `PadicSeq p`.
`Valuation f` is defined to be the valuation of the (`ℚ`-valued) stationary point of `f`. -/
def valuation (f : PadicSeq p) : ℤ :=
if hf : f ≈ 0 then 0 else padicValRat p (f (stationaryPoint hf))
