Theorems · Theorem · commutative algebra

Algebra.IsPushout.out

∀ {R : Type u_1} {S : Type v₃} {inst : CommSemiring R} {inst_1 : CommSemiring S} {inst_2 : Algebra R S} {R' : Type u_6}
  {S' : Type u_7} {inst_3 : CommSemiring R'} {inst_4 : CommSemiring S'} {inst_5 : Algebra R R'} {inst_6 : Algebra S S'}
  {inst_7 : Algebra R' S'} {inst_8 : Algebra R S'} {inst_9 : IsScalarTower R R' S'} {inst_10 : IsScalarTower R S S'}
  [self : Algebra.IsPushout R S R' S'], IsBaseChange S (IsScalarTower.toAlgHom R R' S').toLinearMap

Defined in

Mathlib.RingTheory.IsTensorProduct

Cited by

5 results in Mathlib

Foundations

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

Assumes

Algebra.IsPushout