cast_ne_zero_of_ne_of_prime — Mathlib

English

If R has CharP p and q is a prime with p ≠ q, then (q : R) ≠ 0.

Русский

Если у RCharP p и q — простое число с p ≠ q, то (q : R) ≠ 0.

LaTeX

$$$ \forall R, [CharP R p], Nat.Prime q \rightarrow Ne p q \rightarrow (q : R) \neq 0 $$$

Lean4

/-- If a ring `R` is of characteristic `p`, then for any prime number `q` different from `p`,
it is not zero in `R`. -/
theorem cast_ne_zero_of_ne_of_prime [Nontrivial R] {p q : ℕ} [CharP R p] (hq : q.Prime) (hneq : p ≠ q) : (q : R) ≠ 0 :=
  fun h ↦ by
  rw [cast_eq_zero_iff R p q] at h
  rcases hq.eq_one_or_self_of_dvd _ h with h | h
  · subst h
    exact false_of_nontrivial_of_char_one (R := R)
  · exact hneq h

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