p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q = 0
this : const (padicNorm p) q ≈ 0
⊢ norm (const (padicNorm p) q) = padicNorm p q
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q = 0
⊢ norm (const (padicNorm p) q) = padicNorm p q
have : const (padicNorm p) q ≈ 0 := by simp [hq]; apply Setoid.refl (const (padicNorm p) 0)
p : ℕ
hp : Fact (Nat.Prime p)
this : const (padicNorm p) 0 ≈ 0
⊢ norm (const (padicNorm p) 0) = padicNorm p 0
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q = 0
this : const (padicNorm p) q ≈ 0
⊢ norm (const (padicNorm p) q) = padicNorm p q
subst hq
no goals
p : ℕ
hp : Fact (Nat.Prime p)
this : const (padicNorm p) 0 ≈ 0
⊢ norm (const (padicNorm p) 0) = padicNorm p 0
simp [norm, this]
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q = 0
⊢ 0 ≈ 0
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q = 0
⊢ const (padicNorm p) q ≈ 0
simp [hq]
no goals
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q = 0
⊢ 0 ≈ 0
apply Setoid.refl (const (padicNorm p) 0)
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : ¬q = 0
this : ¬const (padicNorm p) q ≈ 0
⊢ norm (const (padicNorm p) q) = padicNorm p q
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : ¬q = 0
⊢ norm (const (padicNorm p) q) = padicNorm p q
have : ¬const (padicNorm p) q ≈ 0 := not_equiv_zero_const_of_nonzero hq
no goals
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : ¬q = 0
this : ¬const (padicNorm p) q ≈ 0
⊢ norm (const (padicNorm p) q) = padicNorm p q
simp [norm, this]