agda-stdlib/src/Algebra/Module/Properties.agda at e67d1e9a5c3b13e7a2465b7bc1c8c8d2de3045d5 · jamesmckinna/agda-stdlib · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of modules.
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

open import Algebra.Bundles        using (CommutativeRing)
open import Algebra.Module.Bundles using (Module)
open import Level                  using (Level)

module Algebra.Module.Properties
  {r ℓr m ℓm : Level}
  {ring      : CommutativeRing r ℓr}
  (mod       : Module ring m ℓm)
  where

open Module mod
open import Algebra.Module.Properties.Semimodule semimodule public
open import Algebra.Module.Properties.LeftModule leftModule public
  using (identityˡ-uniqueᴹ; identityʳ-uniqueᴹ)
open import Algebra.Properties.Group +ᴹ-group public
  using ()
  renaming (⁻¹-involutive to -ᴹ-involutive)