Def Subbimodule.toSubbimoduleNat

Modification history

2025-07-03 01:14

Mathlib/Algebra/Module/Bimodule.lean

refactor: remove `suppress_compilation` from TensorProduct (#26642) …

Added Subbimodule.toSubbimoduleNat View on Github →

2025-05-02 23:00

Mathlib/Algebra/Module/Bimodule.lean

chore: bump toolchain to v4.20.0-rc2 (#24561)

Deleted Subbimodule.toSubbimoduleNat View on Github →

2023-05-18 15:44

Mathlib/Algebra/Module/Bimodule.lean

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

Added Subbimodule.toSubbimoduleNat View on Github →