Skip to content

Commit

Permalink
doc(NumberTheory/Padics/PadicVal): typo (#11320)
Browse files Browse the repository at this point in the history
Fix a typo.
  • Loading branch information
gaetanserre committed Mar 12, 2024
1 parent bb81b9f commit c489838
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/NumberTheory/Padics/PadicVal.lean
Expand Up @@ -72,7 +72,7 @@ open Rat
open multiplicity

/-- For `p ≠ 1`, the `p`-adic valuation of a natural `n ≠ 0` is the largest natural number `k` such
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`. -/
def padicValNat (p : ℕ) (n : ℕ) : ℕ :=
if h : p ≠ 10 < n then (multiplicity p n).get (multiplicity.finite_nat_iff.2 h) else 0
#align padic_val_nat padicValNat
Expand Down

0 comments on commit c489838

Please sign in to comment.