p : ℕ
hp : Fact (Nat.Prime p)
a : PadicSeq p
ha : ¬a ≈ 0
k : ℚ
hk : norm a = padicNorm p k
hk' : k ≠ 0
⊢ ∃ z, norm a = ↑p ^ (-z)
p : ℕ
hp : Fact (Nat.Prime p)
a : PadicSeq p
ha : ¬a ≈ 0
⊢ ∃ z, norm a = ↑p ^ (-z)
let ⟨k, hk, hk'⟩ := norm_eq_norm_app_of_nonzero ha
no goals
p : ℕ
hp : Fact (Nat.Prime p)
a : PadicSeq p
ha : ¬a ≈ 0
k : ℚ
hk : norm a = padicNorm p k
hk' : k ≠ 0
⊢ ∃ z, norm a = ↑p ^ (-z)
simpa [hk] using padicNorm.values_discrete hk'