Theorems · Theorem · ring theory

Pi.nonUnitalRingHom_injective

Deprecated since 2026-05-30Use NonUnitalRingHom.pi_injective instead.

∀ {I : Type u} {f : I → Type u_1} {γ : Type u_2} [Nonempty I] [inst : (i : I) → NonUnitalNonAssocSemiring (f i)]
  [inst_1 : NonUnitalNonAssocSemiring γ] (g : (i : I) → γ →ₙ+* f i),
  (∀ (i : I), Function.Injective ⇑(g i)) → Function.Injective ⇑(NonUnitalRingHom.pi g)

Alias of NonUnitalRingHom.pi_injective.

Defined in

Mathlib.Algebra.Ring.Pi

Cited by

0 results in Mathlib

Foundations

Depth 17 from the axioms · uses Quot.sound

Assumes

NonemptyNonUnitalNonAssocSemiringNonUnitalNonAssocSemiring