Invertible integers in a local ring

A natural number is invertible in a commutative local ring exactly when the characteristic of the residue field does not divide it, since an element of a local ring is a unit exactly when its residue is nonzero.

Main results

• IsLocalRing.isUnit_natCast_iff_not_dvd: n is a unit of a local ring R exactly when the residue characteristic of R does not divide n.

@[simp]

theorem IsLocalRing.isUnit_natCast_iff_not_dvd {R : Type u_1} [CommRing R] [IsLocalRing R] {n : ℕ} : IsUnit ↑n ↔ ¬ringChar (ResidueField R) ∣ n

A natural number is invertible in a commutative local ring exactly when the residue characteristic does not divide it.