no goals
p : ℕ
q : ℚ
hq : q = 0
⊢ 0 ≤ padicNorm p q
simp [hq, padicNorm]
p : ℕ
q : ℚ
hq : ¬q = 0
⊢ 0 ≤ if q = 0 then 0 else ↑p ^ (-padicValRat p q)
p : ℕ
q : ℚ
hq : ¬q = 0
⊢ 0 ≤ padicNorm p q
unfold padicNorm
p : ℕ
q : ℚ
hq : ¬q = 0
⊢ 0 ≤ ↑p ^ (-padicValRat p q)
p : ℕ
q : ℚ
hq : ¬q = 0
⊢ 0 ≤ if q = 0 then 0 else ↑p ^ (-padicValRat p q)
split_ifs
case ha
p : ℕ
q : ℚ
hq : ¬q = 0
⊢ 0 ≤ ↑p
p : ℕ
q : ℚ
hq : ¬q = 0
⊢ 0 ≤ ↑p ^ (-padicValRat p q)
apply zpow_nonneg
no goals
case ha
p : ℕ
q : ℚ
hq : ¬q = 0
⊢ 0 ≤ ↑p
exact_mod_cast Nat.zero_le _