p : ℕ
hp : Fact (Nat.Prime p)
h1 : ¬1 ≈ 0
⊢ norm 1 = 1
p : ℕ
hp : Fact (Nat.Prime p)
⊢ norm 1 = 1
have h1 : ¬(1 : PadicSeq p) ≈ 0 := one_not_equiv_zero _
no goals
p : ℕ
hp : Fact (Nat.Prime p)
h1 : ¬1 ≈ 0
⊢ norm 1 = 1
simp [h1, norm, hp.1.one_lt]