Theorems · Definition · commutative algebra

Subring.prod

{R : Type u} →
  {S : Type v} → [inst : NonAssocRing R] → [inst_1 : NonAssocRing S] → Subring R → Subring S → Subring (R × S)

Given Subrings s, t of rings R, S respectively, s.prod t is s ×̂ t as a subring of R × S.

Defined in

Mathlib.Algebra.Ring.Subring.Basic

Cited by

11 results in Mathlib

Foundations

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

Assumes

NonAssocRingNonAssocRing