Commit 2024-10-01 14:56 a9d07e8c

feat(RingTheory/IsTensorProduct): cancel pushout square on the left (#17028) Given a commutative diagram of rings

  R  →  S  →  T
  ↓     ↓     ↓
  R' →  S' →  T'

where the left-hand square is a pushout and the big rectangle is a pushout, we show that then also the right-hand square is a pushout.