Theorem IsLocalizedModule.isScalarTower_module

Modification history

2025-04-13 08:52
Mathlib/Algebra/Module/LocalizedModule/Basic.lean
feat(RingTheory): base change commutes with finite products (#22339) …
Added IsLocalizedModule.isScalarTower_moduleView on Github →