p✝ q : ℕ
p_prime : Fact (Nat.Prime p✝)
q_prime : Fact (Nat.Prime q)
neq : p✝ ≠ q
p : padicValRat p✝ ↑q = 0
⊢ padicNorm p✝ ↑q = 1
p q : ℕ
p_prime : Fact (Nat.Prime p)
q_prime : Fact (Nat.Prime q)
neq : p ≠ q
⊢ padicNorm p ↑q = 1
have p : padicValRat p q = 0 := by exact_mod_cast padicValNat_primes neq
p✝ q : ℕ
p_prime : Fact (Nat.Prime p✝)
q_prime : Fact (Nat.Prime q)
neq : p✝ ≠ q
p : padicValRat p✝ ↑q = 0
⊢ (if ↑q = 0 then 0 else ↑p✝ ^ (-0)) = 1
p✝ q : ℕ
p_prime : Fact (Nat.Prime p✝)
q_prime : Fact (Nat.Prime q)
neq : p✝ ≠ q
p : padicValRat p✝ ↑q = 0
⊢ padicNorm p✝ ↑q = 1
rw [padicNorm, p]
no goals
p✝ q : ℕ
p_prime : Fact (Nat.Prime p✝)
q_prime : Fact (Nat.Prime q)
neq : p✝ ≠ q
p : padicValRat p✝ ↑q = 0
⊢ (if ↑q = 0 then 0 else ↑p✝ ^ (-0)) = 1
simp [q_prime.1.ne_zero]
no goals
p q : ℕ
p_prime : Fact (Nat.Prime p)
q_prime : Fact (Nat.Prime q)
neq : p ≠ q
⊢ padicValRat p ↑q = 0
exact_mod_cast padicValNat_primes neq