------------------------------------------------------------------------
-- 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.Bimodule bimodule public
using (inverseˡ-uniqueᴹ; inverseʳ-uniqueᴹ; -ᴹ-involutive)
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4