not_ringChar_dvd_of_invertible — Mathlib

English

For any t ∈ ℕ, if t is invertible in R and R is nontrivial, then ringChar R ∤ t.

Русский

Для любого t ∈ ℕ, если t обратим в R и R не тривиально, то ringChar R не делит t.

LaTeX

$$$\forall t \in \mathbb{N}, \; (Invertible\,(t:R)) \Rightarrow (Nontrivial\,R) \Rightarrow ringChar(R) \nmid t$$$

Lean4

theorem not_ringChar_dvd_of_invertible {t : ℕ} [Invertible (t : R)] [Nontrivial R] : ¬ringChar R ∣ t :=
  by
  rw [← ringChar.spec, ← Ne]
  exact Invertible.ne_zero (t : R)

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