------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of bimodules.
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Algebra.Bundles using (Ring)
open import Algebra.Module.Bundles using (Bimodule)
open import Level using (Level)
module Algebra.Module.Properties.Bimodule
{r ℓr s ℓs m ℓm : Level}
{ringR : Ring r ℓr} {ringS : Ring s ℓs}
(mod : Bimodule ringR ringS m ℓm)
where
open Bimodule mod
open import Algebra.Module.Properties.LeftModule leftModule 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