p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ z ∈ nonunits ℤ_[p] ↔ ‖z‖ ≤ 1 ∧ ‖z‖ ≠ 1
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ z ∈ nonunits ℤ_[p] ↔ ‖z‖ < 1
rw [lt_iff_le_and_ne]
no goals
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ z ∈ nonunits ℤ_[p] ↔ ‖z‖ ≤ 1 ∧ ‖z‖ ≠ 1
simp [norm_le_one z, nonunits, isUnit_iff]