Theorem Submodule.mulMap_one_left_eq

Modification history

2024-10-26 13:22

Mathlib/LinearAlgebra/TensorProduct/Submodule.lean

refactor: change the definition of `1 : Submodule R A` to the range of `(· • 1)` (#18092) …

Modified Submodule.mulMap_one_left_eq View on Github →

2024-06-26 11:25

Mathlib/LinearAlgebra/TensorProduct/Submodule.lean

feat(LinearAlgebra/TensorProduct/Submodule): add some linear maps induced by multiplication for submodules (#12498) …

Added Submodule.mulMap_one_left_eq View on Github →