isUnit_intCast_iff — Mathlib

English

For prime p, IsUnit (z : R) iff ¬↑p ∣ z for z ∈ ℤ.

Русский

Пусть p — простое. Тогда IsUnit (z : R) эквивалентно ¬(p ∣ z) для z ∈ ℤ.

LaTeX

$$IsUnit(z.cast) \iff ¬ p \mid z$$

Lean4

theorem isUnit_intCast_iff {z : ℤ} (hp : p.Prime) : IsUnit (z : R) ↔ ¬↑p ∣ z :=
  by
  obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg
  · simp [CharP.isUnit_natCast_iff hp, Int.ofNat_dvd]
  · simp [CharP.isUnit_natCast_iff hp, Int.dvd_neg, Int.ofNat_dvd]

Похожие утверждения