isUnit_natCast_iff — Mathlib

English

Let p be prime. For any n ∈ ℕ, IsUnit (n : R) holds iff ¬ p ∣ n.

Русский

Пусть p — простое. Тогда IsUnit (n : R) эквивалентно не делит ли p число n.

LaTeX

$$IsUnit(n.cast) \iff \neg p \mid n$$

Lean4

theorem isUnit_natCast_iff {n : ℕ} (hp : p.Prime) : IsUnit (n : R) ↔ ¬p ∣ n
    where
  mp
    h := by
    have := CharP.nontrivial_of_char_ne_one (R := R) hp.ne_one
    rw [← CharP.cast_eq_zero_iff (R := R)]
    exact h.ne_zero
  mpr
    not_dvd :=
    letI := invertibleOfCoprime (R := R) (hp.coprime_iff_not_dvd.2 not_dvd).symm
    isUnit_of_invertible _

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