Commit 2023-05-18 15:44 4c4a23d3

View on Github →

feat: port Algebra.Module.Bimodule (#4077)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Module/Bimodule.lean

added def Subbimodule.baseChange

added def Subbimodule.mk

added theorem Subbimodule.smul_mem'

added theorem Subbimodule.smul_mem

added def Subbimodule.toSubbimoduleInt

added def Subbimodule.toSubbimoduleNat

added def Subbimodule.toSubmodule'

added def Subbimodule.toSubmodule