case a
p : ℕ
hp : Fact (Nat.Prime p)
⊢ maximalIdeal ℤ_[p] ≤ Ideal.span {↑p}

case a
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Ideal.span {↑p} ≤ maximalIdeal ℤ_[p]
p : ℕ
hp : Fact (Nat.Prime p)
⊢ maximalIdeal ℤ_[p] = Ideal.span {↑p}
apply le_antisymm
case a
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ∈ maximalIdeal ℤ_[p]
⊢ x ∈ Ideal.span {↑p}
case a
p : ℕ
hp : Fact (Nat.Prime p)
⊢ maximalIdeal ℤ_[p] ≤ Ideal.span {↑p}
intro x hx
case a
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : ‖x‖ < 1
⊢ x ∈ Ideal.span {↑p}
case a
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ∈ maximalIdeal ℤ_[p]
⊢ x ∈ Ideal.span {↑p}
simp only [LocalRing.mem_maximalIdeal, mem_nonunits] at hx
no goals
case a
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : ‖x‖ < 1
⊢ x ∈ Ideal.span {↑p}
rwa [Ideal.mem_span_singleton, ← norm_lt_one_iff_dvd]
case a
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ↑p ∈ ↑(maximalIdeal ℤ_[p])
case a
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Ideal.span {↑p} ≤ maximalIdeal ℤ_[p]
rw [Ideal.span_le, Set.singleton_subset_iff]
no goals
case a
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ↑p ∈ ↑(maximalIdeal ℤ_[p])
exact p_nonnunit