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/BaseChange.agda | |
| parent | 9a65579633967a0c02b912e6baa3e575a02b868f (diff) | |
Add more matrix operations
Diffstat (limited to 'Data/Matrix/BaseChange.agda')
| -rw-r--r-- | Data/Matrix/BaseChange.agda | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Data/Matrix/BaseChange.agda b/Data/Matrix/BaseChange.agda index 2135c13..04b9f9c 100644 --- a/Data/Matrix/BaseChange.agda +++ b/Data/Matrix/BaseChange.agda @@ -95,7 +95,7 @@ resp = cong (Mat.₁ func) ⟨ε⟩-homo {A} = MonoidHomomorphism.ε-homo (MonEndo.mapₘ A (mk-⇒ +-monoidHomomorphism)) opaque - unfolding I _ᵀ _∷ₕ_ Endo.mapₛ + unfolding I _∷ₕ_ Endo.mapₛ ident : {A : ℕ} → change (I R) MatS.≋ I S {A} ident {zero} = PW.[] ident {suc A} = (1#-homo PW.∷ ⟨ε⟩-homo) PW.∷ map-⟨ε⟩∷ₕI |