Commit 2025-10-24 11:00 50c7f343

View on Github →

feat(RingTheory/IsTensorProduct): add IsPushout.cancelBaseChange (#28772) This is a cancel-on-the-left version of AlgebraTensorModule.cancelBaseChange.

Estimated changes

Modified Mathlib/Algebra/Algebra/Basic.lean

Modified Mathlib/Algebra/RingQuot.lean

Modified Mathlib/Analysis/RCLike/Inner.lean

Modified Mathlib/RingTheory/IsTensorProduct.lean

added def Algebra.IsPushout.cancelBaseChange

added def Algebra.IsPushout.cancelBaseChangeAux

added theorem Algebra.IsPushout.cancelBaseChangeAux_symm_tmul

added theorem Algebra.IsPushout.cancelBaseChange_symm_tmul

added theorem Algebra.IsPushout.cancelBaseChange_tmul