p : ℕ
hp : Fact (Nat.Prime p)
this : (↑p)⁻¹ < 1
⊢ ↑p ∈ nonunits ℤ_[p]
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ↑p ∈ nonunits ℤ_[p]
have : (p : ℝ)⁻¹ < 1 := inv_lt_one <| by exact_mod_cast hp.1.one_lt
no goals
p : ℕ
hp : Fact (Nat.Prime p)
this : (↑p)⁻¹ < 1
⊢ ↑p ∈ nonunits ℤ_[p]
rwa [← norm_p, ← mem_nonunits] at this
no goals
p : ℕ
hp : Fact (Nat.Prime p)
⊢ 1 < ↑p
exact_mod_cast hp.1.one_lt