intCast_eq_zero_iff — Mathlib

English

If R has CharZero (characteristic zero), then CharP R 0 holds.

Русский

Если в кольце R характеристика ноль, то CharP R 0 выполняется.

LaTeX

$$$[CharZero(R)] \Rightarrow CharP(R, 0).$$$

Lean4

theorem intCast_eq_zero_iff (a : ℤ) : (a : R) = 0 ↔ (p : ℤ) ∣ a :=
  by
  rcases lt_trichotomy a 0 with (h | rfl | h)
  · rw [← neg_eq_zero, ← Int.cast_neg, ← Int.dvd_neg]
    lift -a to ℕ using Int.neg_nonneg.mpr (le_of_lt h) with b
    rw [Int.cast_natCast, CharP.cast_eq_zero_iff R p, Int.natCast_dvd_natCast]
  · simp only [Int.cast_zero, Int.dvd_zero]
  · lift a to ℕ using le_of_lt h with b
    rw [Int.cast_natCast, CharP.cast_eq_zero_iff R p, Int.natCast_dvd_natCast]

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