Theorems · Definition · ring theory

Pi.nonUnitalRingHom

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

{I : Type u} →
  {f : I → Type u_1} →
    {γ : Type u_2} →
      [inst : (i : I) → NonUnitalNonAssocSemiring (f i)] →
        [inst_1 : NonUnitalNonAssocSemiring γ] → ((i : I) → γ →ₙ+* f i) → γ →ₙ+* (i : I) → f i

Alias of NonUnitalRingHom.pi. A family of non-unital ring homomorphisms f a : γ →ₙ+* β a defines a non-unital ring homomorphism NonUnitalRingHom.pi f : γ →+* Π a, β a given by NonUnitalRingHom.pi f x b = f b x.

Defined in

Mathlib.Algebra.Ring.Pi

Cited by

0 results in Mathlib

Foundations

Depth 16 from the axioms · uses Quot.sound

Assumes

NonUnitalNonAssocSemiringNonUnitalNonAssocSemiring