Theorems · Definition · ring theory

RingHom.pi

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

A family of ring homomorphisms f a : γ →+* β a defines a ring homomorphism RingHom.pi f : γ →+* Π a, β a given by RingHom.pi f x b = f b x.

Defined in

Mathlib.Algebra.Ring.Pi

Cited by

26 results in Mathlib

Foundations

Depth 16 from the axioms · uses Quot.sound

Assumes

NonAssocSemiringNonAssocSemiring