diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-08-22 14:52:16 -0500 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-08-22 14:52:16 -0500 |
| commit | f7091746dcae0aacd0fc8c8971d6dc5a748e7bc5 (patch) | |
| tree | 9966acfbd9584af65d1f20f99e051bdc94ecd63b /Data/Matrix/SemiadditiveDagger.agda | |
| parent | 9a65579633967a0c02b912e6baa3e575a02b868f (diff) | |
Add more matrix operations
Diffstat (limited to 'Data/Matrix/SemiadditiveDagger.agda')
| -rw-r--r-- | Data/Matrix/SemiadditiveDagger.agda | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/Data/Matrix/SemiadditiveDagger.agda b/Data/Matrix/SemiadditiveDagger.agda index 017f05f..7ebc5da 100644 --- a/Data/Matrix/SemiadditiveDagger.agda +++ b/Data/Matrix/SemiadditiveDagger.agda @@ -26,7 +26,7 @@ open import Category.Semiadditive using (Semiadditive) open import Data.Matrix.Category R.semiring using (Mat; _·_; ≑-·; ·-Iˡ; ·-Iʳ; ·-𝟎ˡ; ·-𝟎ʳ; ·-∥; ∥-·-≑; ·-resp-≋; ·-assoc) open import Data.Matrix.Core R.setoid using (Matrix; Matrixₛ; _≋_; module ≋; ∥-cong; ≑-cong; ᵀ-cong) open import Data.Matrix.Monoid R.+-monoid using (𝟎; 𝟎ᵀ; 𝟎≑𝟎; 𝟎∥𝟎; _[+]_; [+]-cong; [+]-𝟎ˡ; [+]-𝟎ʳ) -open import Data.Matrix.Raw using (_ᵀ; _ᵀᵀ; mapRows; []ᵥ; []ᵥ-∥; []ₕ; []ₕ-!; []ₕ-≑; _∷ᵥ_; _∷ₕ_; ∷ᵥ-ᵀ; _∥_; _≑_; ∷ₕ-ᵀ; ∷ₕ-≑; []ᵥ-ᵀ; head-∷-tailₕ; headₕ; tailₕ; ∷ₕ-∥; ∷ᵥ-≑; []ᵥ-!) +open import Data.Matrix.Raw using (_ᵀ; _ᵀᵀ; []ᵥ; []ᵥ-∥; []ₕ; []ₕ-!; []ₕ-≑; _∷ᵥ_; _∷ₕ_; ∷ᵥ-ᵀ; _∥_; _≑_; ∷ₕ-ᵀ; ∷ₕ-≑; []ᵥ-ᵀ; head-∷-tailₕ; headₕ; tailₕ; ∷ₕ-∥; ∷ᵥ-≑; []ᵥ-!) open import Data.Matrix.Semiadditive R.semiring using (Mat-Semiadditive) open import Data.Matrix.Transform R.semiring using (I; Iᵀ; [_]_; _[_]; -[-]ᵀ; [-]--cong; [-]-[]ᵥ; [⟨⟩]-[]ₕ) open import Data.Nat using (ℕ) @@ -56,7 +56,7 @@ opaque ∙-comm (x ∷ V) (w ∷ W) = +-cong (*-comm x w) (∙-comm V W) opaque - unfolding _[_] [_]_ _ᵀ []ᵥ _∷ₕ_ _≋_ _∷ᵥ_ + unfolding _[_] [_]_ []ᵥ _∷ₕ_ _≋_ _∷ᵥ_ [-]-ᵀ : (M : Matrix A B) (V : Vector A) → M [ V ] ≊ [ V ] (M ᵀ) [-]-ᵀ [] V = ≊.sym (≊.reflexive ([-]-[]ᵥ V)) [-]-ᵀ (M₀ ∷ M) V = begin @@ -69,7 +69,7 @@ opaque open ≈-Reasoning (Vectorₛ _) opaque - unfolding []ᵥ mapRows _∷ₕ_ _∷ᵥ_ _ᵀ _≋_ + unfolding []ᵥ _∷ₕ_ _∷ᵥ_ _≋_ ·-ᵀ : {A B C : ℕ} (M : Matrix A B) @@ -95,7 +95,7 @@ opaque ᵀ-involutive M = ≋.reflexive (M ᵀᵀ) opaque - unfolding Matrix _∥_ _ᵀ _≑_ _∷ₕ_ + unfolding _∥_ _≑_ _∷ₕ_ ∥-ᵀ : (M : Matrix A C) (N : Matrix B C) → (M ∥ N) ᵀ ≡ M ᵀ ≑ N ᵀ ∥-ᵀ {A} {zero} {B} [] [] = ≡.sym (replicate-++ A B []) ∥-ᵀ (M₀ ∷ M) (N₀ ∷ N) = begin |