-
Notifications
You must be signed in to change notification settings - Fork 102
Expand file tree
/
Copy pathlinear-algebra.lagda.md
More file actions
108 lines (105 loc) · 6.79 KB
/
Copy pathlinear-algebra.lagda.md
File metadata and controls
108 lines (105 loc) · 6.79 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
# Linear algebra
## Modules in the linear algebra namespace
```agda
module linear-algebra where
open import linear-algebra.addition-linear-maps-left-modules-commutative-rings public
open import linear-algebra.addition-linear-maps-left-modules-rings public
open import linear-algebra.bilinear-forms-real-vector-spaces public
open import linear-algebra.bilinear-maps-left-modules-commutative-rings public
open import linear-algebra.bilinear-maps-left-modules-rings public
open import linear-algebra.cauchy-schwarz-inequality-complex-inner-product-spaces public
open import linear-algebra.cauchy-schwarz-inequality-real-inner-product-spaces public
open import linear-algebra.complex-inner-product-spaces public
open import linear-algebra.complex-vector-spaces public
open import linear-algebra.conjugate-symmetric-sesquilinear-forms-complex-vector-spaces public
open import linear-algebra.constant-matrices public
open import linear-algebra.constant-tuples public
open import linear-algebra.dependent-products-left-modules-commutative-rings public
open import linear-algebra.dependent-products-left-modules-rings public
open import linear-algebra.dependent-products-real-vector-spaces public
open import linear-algebra.dependent-products-vector-spaces public
open import linear-algebra.diagonal-matrices-on-rings public
open import linear-algebra.difference-linear-maps-left-modules-commutative-rings public
open import linear-algebra.difference-linear-maps-left-modules-rings public
open import linear-algebra.dot-product-standard-euclidean-vector-spaces public
open import linear-algebra.duals-left-modules-commutative-rings public
open import linear-algebra.finite-sequences-in-abelian-groups public
open import linear-algebra.finite-sequences-in-commutative-monoids public
open import linear-algebra.finite-sequences-in-commutative-rings public
open import linear-algebra.finite-sequences-in-commutative-semigroups public
open import linear-algebra.finite-sequences-in-commutative-semirings public
open import linear-algebra.finite-sequences-in-euclidean-domains public
open import linear-algebra.finite-sequences-in-groups public
open import linear-algebra.finite-sequences-in-monoids public
open import linear-algebra.finite-sequences-in-rings public
open import linear-algebra.finite-sequences-in-semigroups public
open import linear-algebra.finite-sequences-in-semirings public
open import linear-algebra.function-left-modules-rings public
open import linear-algebra.function-real-vector-spaces public
open import linear-algebra.function-vector-spaces public
open import linear-algebra.functoriality-matrices public
open import linear-algebra.kernels-linear-maps-left-modules-commutative-rings public
open import linear-algebra.kernels-linear-maps-left-modules-rings public
open import linear-algebra.kernels-linear-maps-vector-spaces public
open import linear-algebra.large-left-modules-large-rings public
open import linear-algebra.left-module-linear-maps-left-modules-commutative-rings public
open import linear-algebra.left-modules-commutative-rings public
open import linear-algebra.left-modules-rings public
open import linear-algebra.left-submodules-commutative-rings public
open import linear-algebra.left-submodules-rings public
open import linear-algebra.linear-combinations-tuples-of-vectors-left-modules-rings public
open import linear-algebra.linear-endomaps-left-modules-commutative-rings public
open import linear-algebra.linear-endomaps-left-modules-rings public
open import linear-algebra.linear-endomaps-vector-spaces public
open import linear-algebra.linear-forms-left-modules-commutative-rings public
open import linear-algebra.linear-forms-vector-spaces public
open import linear-algebra.linear-maps-left-modules-commutative-rings public
open import linear-algebra.linear-maps-left-modules-rings public
open import linear-algebra.linear-maps-vector-spaces public
open import linear-algebra.linear-spans-left-modules-rings public
open import linear-algebra.lipschitz-continuity-scalar-multiplication-normed-real-vector-spaces public
open import linear-algebra.lipschitz-maps-normed-real-vector-spaces public
open import linear-algebra.matrices public
open import linear-algebra.matrices-on-rings public
open import linear-algebra.multiplication-matrices public
open import linear-algebra.negation-linear-maps-left-modules-rings public
open import linear-algebra.normed-complex-vector-spaces public
open import linear-algebra.normed-real-algebras public
open import linear-algebra.normed-real-vector-spaces public
open import linear-algebra.orthogonality-bilinear-forms-real-vector-spaces public
open import linear-algebra.orthogonality-real-inner-product-spaces public
open import linear-algebra.precategory-of-left-modules-commutative-rings public
open import linear-algebra.precategory-of-left-modules-rings public
open import linear-algebra.precategory-of-vector-spaces public
open import linear-algebra.preimages-of-left-module-structures-along-homomorphisms-of-rings public
open import linear-algebra.rational-modules public
open import linear-algebra.real-algebras public
open import linear-algebra.real-inner-product-spaces public
open import linear-algebra.real-inner-product-spaces-are-normed public
open import linear-algebra.real-vector-spaces public
open import linear-algebra.right-modules-rings public
open import linear-algebra.scalar-multiplication-linear-maps-left-modules-commutative-rings public
open import linear-algebra.scalar-multiplication-linear-maps-vector-spaces public
open import linear-algebra.scalar-multiplication-matrices public
open import linear-algebra.scalar-multiplication-tuples public
open import linear-algebra.scalar-multiplication-tuples-on-rings public
open import linear-algebra.seminormed-complex-vector-spaces public
open import linear-algebra.seminormed-real-vector-spaces public
open import linear-algebra.sesquilinear-forms-complex-vector-spaces public
open import linear-algebra.standard-euclidean-inner-product-spaces public
open import linear-algebra.standard-euclidean-vector-spaces public
open import linear-algebra.subsets-left-modules-commutative-rings public
open import linear-algebra.subsets-left-modules-rings public
open import linear-algebra.subspaces-vector-spaces public
open import linear-algebra.sums-of-finite-sequences-of-elements-normed-real-vector-spaces public
open import linear-algebra.symmetric-bilinear-forms-real-vector-spaces public
open import linear-algebra.transposition-matrices public
open import linear-algebra.tuples-on-commutative-monoids public
open import linear-algebra.tuples-on-commutative-rings public
open import linear-algebra.tuples-on-commutative-semirings public
open import linear-algebra.tuples-on-euclidean-domains public
open import linear-algebra.tuples-on-monoids public
open import linear-algebra.tuples-on-rings public
open import linear-algebra.tuples-on-semirings public
open import linear-algebra.vector-spaces public
```