Submodules of a module #
In this file we define
Submodule R M
: a subset of aModule
M
that contains zero and is closed with respect to addition and scalar multiplication.Subspace k M
: an abbreviation forSubmodule
assuming thatk
is aField
.
Tags #
submodule, subspace, linear map
A submodule of a module is one which is closed under vector operations. This is a sufficient condition for the subset of vectors in the submodule to themselves form a module.
Instances For
Equations
The actual Submodule
obtained from an element of a SMulMemClass
and AddSubmonoidClass
.
Equations
Instances For
Alias of Submodule.toAddSubmonoid_inj
.
Alias of Submodule.toSubMulAction_inj
.
A submodule of a Module
is a Module
.
Equations
This can't be an instance because Lean wouldn't know how to find R
, but we can still use
this to manually derive Module
on specific types.
Equations
Instances For
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Reinterpret a submodule as an additive subgroup.
Equations
Instances For
Alias of Submodule.toAddSubgroup_inj
.