instIsLocalHomRingHomOfNontrivial

English

Any ring homomorphism from a local ring to a nontrivial ZMod n is a local hom.

Русский

Любой гомоморфизм кольца из локального кольца в ненулевой ZMod n является локальным гомоморфизмом.

LaTeX

$$$\forall n>0\; (f: R \to\mathbb{Z}/n\mathbb{Z}),\; \text{IsLocalHom}(f)$$$

Lean4

/-- Every ring hom `f : K →+* R` from a division ring `K` to a nontrivial ring `R` is a
local ring hom. -/
instance (priority := 100) {K R} [DivisionRing K] [CommRing R] [Nontrivial R] (f : K →+* R) : IsLocalHom f where
  map_nonunit r hr := by simpa only [isUnit_iff_ne_zero, ne_eq, map_eq_zero] using hr.ne_zero

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