English
A prime p is a unit in a commutative ring R with nonzero characteristic iff p does not divide the characteristic of R.
Русский
Простое число p является единицей в коммутативном кольце R с ненулевой характеристикой тогда и только тогда, когда p не делит характеристику R.
LaTeX
$$$\text{IsUnit}(p: R) \iff \neg p \mid \operatorname{ringChar}(R) \quad\text{(assuming } \operatorname{ringChar}(R) \neq 0\text{)}$$$
Lean4
/-- A prime `p` is a unit in a commutative ring `R` of nonzero characteristic iff it does not divide
the characteristic. -/
theorem isUnit_iff_not_dvd_char_of_ringChar_ne_zero (R : Type*) [CommRing R] (p : ℕ) [Fact p.Prime]
(hR : ringChar R ≠ 0) : IsUnit (p : R) ↔ ¬p ∣ ringChar R :=
by
have hch := CharP.cast_eq_zero R (ringChar R)
have hp : p.Prime := Fact.out
constructor
· rintro h₁ ⟨q, hq⟩
rcases IsUnit.exists_left_inv h₁ with ⟨a, ha⟩
have h₃ : ¬ringChar R ∣ q := by
rintro ⟨r, hr⟩
rw [hr, ← mul_assoc, mul_comm p, mul_assoc] at hq
nth_rw 1 [← mul_one (ringChar R)] at hq
exact Nat.Prime.not_dvd_one hp ⟨r, mul_left_cancel₀ hR hq⟩
have h₄ := mt (CharP.intCast_eq_zero_iff R (ringChar R) q).mp
apply_fun ((↑) : ℕ → R) at hq
apply_fun (· * ·) a at hq
rw [Nat.cast_mul, hch, mul_zero, ← mul_assoc, ha, one_mul] at hq
norm_cast at h₄
exact h₄ h₃ hq.symm
· intro h
rcases (hp.coprime_iff_not_dvd.mpr h).isCoprime with ⟨a, b, hab⟩
apply_fun ((↑) : ℤ → R) at hab
push_cast at hab
rw [hch, mul_zero, add_zero, mul_comm] at hab
exact isUnit_of_mul_eq_one (p : R) a hab
