linear-algebra/Everything.agda at master · felko/linear-algebra · GitHub

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
module Everything where

import Algebra.Structures.Field
import Algebra.Structures.Bundles.Field

import Algebra.Linear.Core

import Algebra.Linear.Space
import Algebra.Linear.Space.Hom
import Algebra.Linear.Space.Product
import Algebra.Linear.Space.FiniteDimensional
import Algebra.Linear.Space.FiniteDimensional.Hom
import Algebra.Linear.Space.FiniteDimensional.Product

import Algebra.Linear.Construct
import Algebra.Linear.Construct.Vector
import Algebra.Linear.Construct.Matrix

import Algebra.Linear.Morphism
import Algebra.Linear.Morphism.Definitions
import Algebra.Linear.Morphism.VectorSpace
import Algebra.Linear.Morphism.Bundles
import Algebra.Linear.Morphism.Bundles.VectorSpace

import Algebra.Linear.Structures
import Algebra.Linear.Structures.VectorSpace
import Algebra.Linear.Structures.FiniteDimensional
import Algebra.Linear.Structures.Bundles
import Algebra.Linear.Structures.Bundles.FiniteDimensional