case pos
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
hx : x = 0
⊢ ‖x‖ ≤ ↑p ^ (-↑n) ↔ x ∈ Ideal.span {↑p ^ n}

case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
hx : ¬x = 0
⊢ ‖x‖ ≤ ↑p ^ (-↑n) ↔ x ∈ Ideal.span {↑p ^ n}
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
⊢ ‖x‖ ≤ ↑p ^ (-↑n) ↔ x ∈ Ideal.span {↑p ^ n}
by_cases hx : x = 0
no goals
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
hx : ¬x = 0
⊢ ‖x‖ ≤ ↑p ^ (-↑n) ↔ x ∈ Ideal.span {↑p ^ n}
rw [norm_le_pow_iff_le_valuation x hx, mem_span_pow_iff_le_valuation x hx]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ‖0‖ ≤ ↑p ^ (-↑n) ↔ 0 ∈ Ideal.span {↑p ^ n}
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
hx : x = 0
⊢ ‖x‖ ≤ ↑p ^ (-↑n) ↔ x ∈ Ideal.span {↑p ^ n}
subst hx
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ 0 ≤ ↑p ^ n
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ‖0‖ ≤ ↑p ^ (-↑n) ↔ 0 ∈ Ideal.span {↑p ^ n}
simp only [norm_zero, zpow_neg, zpow_ofNat, inv_nonneg, iff_true_iff, Submodule.zero_mem]
no goals
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ 0 ≤ ↑p ^ n
exact_mod_cast Nat.zero_le _