invertibleOfCharPNotDvd — Mathlib

English

Same as above with a simp variant.

Русский

То же самое с упрощённой версией.

LaTeX

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

Lean4

/-- A natural number `t` is invertible in a semifield `K` of characteristic `p` if `p` does not
divide `t`. -/
def invertibleOfCharPNotDvd {p : ℕ} [CharP K p] {t : ℕ} (not_dvd : ¬p ∣ t) : Invertible (t : K) :=
  invertibleOfNonzero fun h =>
    not_dvd
      ((CharP.cast_eq_zero_iff K p t).mp h)
        -- warning: this could potentially loop with `Invertible.ne_zero` - if there are weird type-class
        -- loops, watch out for that.

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