Theorems · Definition · commutative algebra

NonUnitalRingHom.prod

{R : Type u_1} →
  {S : Type u_3} →
    {T : Type u_5} →
      [inst : NonUnitalNonAssocSemiring R] →
        [inst_1 : NonUnitalNonAssocSemiring S] →
          [inst_2 : NonUnitalNonAssocSemiring T] → (R →ₙ+* S) → (R →ₙ+* T) → R →ₙ+* S × T

Combine two non-unital ring homomorphisms f : R →ₙ+* S, g : R →ₙ+* T into f.prod g : R →ₙ+* S × T given by (f.prod g) x = (f x, g x)

Defined in

Mathlib.Algebra.Ring.Prod

Cited by

6 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext, Quot.sound

Assumes

NonUnitalNonAssocSemiringNonUnitalNonAssocSemiringNonUnitalNonAssocSemiring