ofNat_eq_zero' — Mathlib

English

If p|a and a is large enough (a ≥ 2), then the image of a in R is zero, given CharP R p.

Русский

Если p делит a и a достаточно велико (a ≥ 2), то образ a в R равен нулю при CharP R p.

LaTeX

$$$p \mid a \quad\Rightarrow\quad (\mathrm{ofNat}(a) : R) = 0 \quad\text{for } a \text{ with } a \ge 2.$$$

Lean4

theorem _root_.CharP.ofNat_eq_zero' (p : ℕ) [CharP R p] (a : ℕ) [a.AtLeastTwo] (h : p ∣ a) : (ofNat(a) : R) = 0 := by
  rwa [← CharP.cast_eq_zero_iff R p] at h

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