Theorems · Theorem · commutative algebra

IsLocalRing.of_injective

∀ {R : Type u_2} {S : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [IsLocalRing S] {f : R →+* S},
  Function.Injective ⇑f → (∀ a ∈ nonZeroDivisors R, IsUnit a) → IsLocalRing R

If a (semi)ring R in which every element is either invertible or a zero divisor embeds in a local (semi)ring S, then R is local.

Defined in

Mathlib.RingTheory.LocalRing.Subring

Cited by

2 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext, Quot.sound

Assumes

SemiringSemiringIsLocalRing