------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of left modules.
------------------------------------------------------------------------

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

open import Algebra.Bundles        using (Ring)
open import Algebra.Module.Bundles using (LeftModule)
open import Level                  using (Level)

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

open Ring       ring
open LeftModule mod
open import Algebra.Properties.AbelianGroup +ᴹ-abelianGroup public
  using ()
  renaming (inverseˡ-unique to inverseˡ-uniqueᴹ
           ; inverseʳ-unique to inverseʳ-uniqueᴹ
           ; ⁻¹-involutive to -ᴹ-involutive)