We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 60ec43d commit fc09926Copy full SHA for fc09926
Mathlib/NumberTheory/Padics/PadicVal.lean
@@ -72,7 +72,7 @@ open Rat
72
open multiplicity
73
74
/-- For `p ≠ 1`, the `p`-adic valuation of a natural `n ≠ 0` is the largest natural number `k` such
75
-that `p^k` divides `z`. If `n = 0` or `p = 1`, then `padicValNat p q` defaults to `0`. -/
+that `p^k` divides `n`. If `n = 0` or `p = 1`, then `padicValNat p q` defaults to `0`. -/
76
def padicValNat (p : ℕ) (n : ℕ) : ℕ :=
77
if h : p ≠ 1 ∧ 0 < n then (multiplicity p n).get (multiplicity.finite_nat_iff.2 h) else 0
78
#align padic_val_nat padicValNat
0 commit comments