injective — Mathlib

English

If R is a simple ring and S is a nontrivial semiring, then any ring homomorphism f: R →+* S is injective.

Русский

Пусть R простое кольцо и S ненулевой полусколь; тогда любой кольцевой гомоморфизм f: R →+* S инъективен.

LaTeX

$$If R is a simple ring and S is nontrivial, then for any f: R →+* S, f is Injective.$$

Lean4

protected theorem _root_.RingHom.injective {R S : Type*} [NonAssocRing R] [IsSimpleRing R] [NonAssocSemiring S]
    [Nontrivial S] (f : R →+* S) : Function.Injective f :=
  injective_ringHom_or_subsingleton_codomain f |>.resolve_right fun r => not_subsingleton _ r

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