Commit 2025-04-13 08:52 19b2d88b

View on Github →

feat(RingTheory): base change commutes with finite products (#22339) and in particular with localizations of modules.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/LocalizedModule/Basic.lean

added theorem IsLocalizedModule.isScalarTower_module

Created Mathlib/RingTheory/TensorProduct/IsBaseChangePi.lean

added theorem IsBaseChange.pi

added theorem IsBaseChange.prodMap