p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : f + g ≈ 0
this : LimZero (f + g - 0)
⊢ norm f = norm g
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : f + g ≈ 0
⊢ norm f = norm g
have : LimZero (f + g - 0) := h
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : f + g ≈ 0
this✝ : LimZero (f + g - 0)
this : f ≈ -g
⊢ norm f = norm g
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : f + g ≈ 0
this : LimZero (f + g - 0)
⊢ norm f = norm g
have : f ≈ -g := show LimZero (f - -g) by simpa only [sub_zero, sub_neg_eq_add]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : f + g ≈ 0
this✝¹ : LimZero (f + g - 0)
this✝ : f ≈ -g
this : norm f = norm (-g)
⊢ norm f = norm g
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : f + g ≈ 0
this✝ : LimZero (f + g - 0)
this : f ≈ -g
⊢ norm f = norm g
have : f.norm = (-g).norm := norm_equiv this
no goals
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : f + g ≈ 0
this✝¹ : LimZero (f + g - 0)
this✝ : f ≈ -g
this : norm f = norm (-g)
⊢ norm f = norm g
simpa only [norm_neg] using this
no goals
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : f + g ≈ 0
this : LimZero (f + g - 0)
⊢ LimZero (f - -g)
simpa only [sub_zero, sub_neg_eq_add]