nonUnitalRingHom_injective — Mathlib

English

Let I be a nonempty type and each f(i) a (non-unital) semiring. If g(i) are injective RingHom/NonUnitalRingHom components, then the Pi construction is injective.

Русский

Пусть I непустое множество, каждый f(i) — полукольцо без единицы. Если каждое g(i) инъективно, то объединяющий Π-гомоморфизм инъективен.

LaTeX

$$$(\forall i, Injective (g(i)))\Rightarrow Injective (Pi.nonUnitalRingHom g)$$$

Lean4

theorem nonUnitalRingHom_injective {γ : Type w} [Nonempty I] [∀ i, NonUnitalNonAssocSemiring (f i)]
    [NonUnitalNonAssocSemiring γ] (g : ∀ i, γ →ₙ+* f i) (hg : ∀ i, Function.Injective (g i)) :
    Function.Injective (Pi.nonUnitalRingHom g) :=
  mulHom_injective (fun i => (g i).toMulHom) hg

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