English
Let R ⊆ R' ⊆ S be subrings of a ring S with S local. If every a ∈ R⁰ is a unit in R, then R is local.
Русский
Пусть $R, R' \\subseteq S$ — подпорядки кольца $S$ с локальным $S$. Если для каждого $a\\in R^\\circ$ верно, что $a$ является единицей в $R$, то $R$ локально.
LaTeX
$$$IsLocalRing(S) \\Rightarrow (R \\le R') \\Rightarrow (\\forall a \\in R^{\\circ}, IsUnit(a)) \\Rightarrow IsLocalRing(R)$$$
Lean4
/-- If in a sub(semi)ring `R` of a local (semi)ring `R'` every element is either
invertible or a zero divisor, then `R` is local.
This version is for `R` and `R'` that are both sub(semi)rings of a (semi)ring `S`. -/
theorem of_subring' {R R' : Subsemiring S} [IsLocalRing R'] (inc : R ≤ R') (h : ∀ a, a ∈ R⁰ → IsUnit a) :
IsLocalRing R :=
of_injective (Subsemiring.inclusion_injective inc) h
