Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-08-12 16:58
58cef51f
View on Github →
feat(algebra/module/bimodule): basic definitions for subbimodules (
#14465
)
Estimated changes
Created
src/algebra/module/bimodule.lean
added
def
subbimodule.base_change
added
def
subbimodule.mk
added
theorem
subbimodule.smul_mem'
added
theorem
subbimodule.smul_mem
added
def
subbimodule.to_subbimodule_int
added
def
subbimodule.to_subbimodule_nat
added
def
subbimodule.to_submodule'
added
def
subbimodule.to_submodule
Modified
src/ring_theory/tensor_product.lean
added
def
tensor_product.algebra.module_aux
added
theorem
tensor_product.algebra.module_aux_apply
added
theorem
tensor_product.algebra.smul_def
Modified
test/instance_diamonds.lean