Theorems · Definition · ring theory

NonUnitalRingHom.pi

{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

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

4 results in Mathlib

Foundations

Depth 15 from the axioms · uses Quot.sound

Assumes

NonUnitalNonAssocSemiringNonUnitalNonAssocSemiring