invertibleOfRingCharNotDvd — Mathlib

English

For prime p, IsUnit (z.cast) iff ¬ p ∣ z for z ∈ ℤ with proof variants.

Русский

Пусть p — простое. Тогда IsUnit (z.cast) эквивалентно ¬ p ∣ z для z ∈ ℤ (вариант доказательства).

LaTeX

$$IsUnit(z.cast) \iff \neg p \mid z$$

Lean4

/-- A natural number `t` is invertible in a semifield `K` if the characteristic of `K` does not
divide `t`. -/
def invertibleOfRingCharNotDvd {t : ℕ} (not_dvd : ¬ringChar K ∣ t) : Invertible (t : K) :=
  invertibleOfNonzero fun h => not_dvd ((ringChar.spec K t).mp h)

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