Theorems · Theorem · commutative algebra

RingHom.prod_comp_prodMap

∀ {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} {T : Type u_5} [inst : NonAssocSemiring R]
  [inst_1 : NonAssocSemiring S] [inst_2 : NonAssocSemiring R'] [inst_3 : NonAssocSemiring S']
  [inst_4 : NonAssocSemiring T] (f : T →+* R) (g : T →+* S) (f' : R →+* R') (g' : S →+* S'),
  (f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)

Defined in

Mathlib.Algebra.Ring.Prod

Cited by

0 results in Mathlib

Foundations

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

Assumes

NonAssocSemiringNonAssocSemiringNonAssocSemiringNonAssocSemiringNonAssocSemiring