Add submodules of left modules over rings

CONTRIBUTORS.toml

@@ -275,3 +275,9 @@ github = "arnoudvanderleer"
 displayName = "Ben Connors"
 usernames = [ "Ben Connors" ]
 github = "ben-connors"
+
+[[contributors]]
+displayName = "Šimon Brandner"
+usernames = ["Šimon Brandner"]
+github = "SimonBrandner"
+homepage = "https://simonbrandner.cz/"

src/linear-algebra.lagda.md

@@ -18,6 +18,7 @@ open import linear-algebra.finite-sequences-in-rings public
 open import linear-algebra.finite-sequences-in-semirings public
 open import linear-algebra.functoriality-matrices public
 open import linear-algebra.left-modules-rings public
+open import linear-algebra.left-submodules-rings public
 open import linear-algebra.linear-maps-left-modules-rings public
 open import linear-algebra.matrices public
 open import linear-algebra.matrices-on-rings public
@@ -28,6 +29,7 @@ open import linear-algebra.right-modules-rings public
 open import linear-algebra.scalar-multiplication-matrices public
 open import linear-algebra.scalar-multiplication-tuples public
 open import linear-algebra.scalar-multiplication-tuples-on-rings public
+open import linear-algebra.subsets-left-modules-rings public
 open import linear-algebra.transposition-matrices public
 open import linear-algebra.tuples-on-commutative-monoids public
 open import linear-algebra.tuples-on-commutative-rings public

src/linear-algebra/left-modules-rings.lagda.md

@@ -83,6 +83,9 @@ module _
   type-left-module-Ring : UU l2
   type-left-module-Ring = type-Ab ab-left-module-Ring
 
+  is-set-type-left-module-Ring : is-set type-left-module-Ring
+  is-set-type-left-module-Ring = pr2 set-left-module-Ring
+
   add-left-module-Ring :
     (x y : type-left-module-Ring) → type-left-module-Ring
   add-left-module-Ring = add-Ab ab-left-module-Ring