Units in a local ring of prescribed residue characteristic #
In a local ring O whose maximal ideal contains a prime p (equivalently, of residue
characteristic p), every integer prime to p is a unit.
theorem
isUnit_natCast_of_not_dvd
{O : Type u_1}
[CommRing O]
[IsLocalRing O]
{p : ℕ}
(hp : Nat.Prime p)
(hpmem : ↑p ∈ IsLocalRing.maximalIdeal O)
{n : ℕ}
(hn : ¬p ∣ n)
:
IsUnit ↑n
Integers prime to p are units in a local ring whose maximal ideal contains p
(equivalently, of residue characteristic p).
theorem
isUnit_sub_of_residue_ne
{O : Type u_1}
[CommRing O]
[IsLocalRing O]
{a b : O}
(h : (IsLocalRing.residue O) a ≠ (IsLocalRing.residue O) b)
:
In a local ring, elements with distinct residues differ by a unit.