monlib4/Monlib.lean at main · themathqueen/monlib4 · 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
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
-- This module serves as the root of the `Monlib` library.
-- Import modules here that should be built as part of the library.

import Monlib.LinearAlgebra.End
-- import Monlib.LinearAlgebra.Blackbox
import Monlib.LinearAlgebra.DirectSumFromTo
import Monlib.LinearAlgebra.InnerAut
import Monlib.LinearAlgebra.InvariantSubmodule
import Monlib.LinearAlgebra.IsProj'
import Monlib.LinearAlgebra.IsReal
import Monlib.LinearAlgebra.KroneckerToTensor
import Monlib.LinearAlgebra.LmulRmul
import Monlib.LinearAlgebra.Mul''
import Monlib.LinearAlgebra.MyBimodule
import Monlib.LinearAlgebra.MySpec
import Monlib.LinearAlgebra.Nacgor
import Monlib.LinearAlgebra.OfNorm
import Monlib.LinearAlgebra.PiDirectSum
import Monlib.LinearAlgebra.PiStarOrderedRing
import Monlib.LinearAlgebra.ToMatrixOfEquiv
import Monlib.LinearAlgebra.PosMap_isReal
import Monlib.LinearAlgebra.LinearMapOp

import Monlib.Other.Sonia

import Monlib.Preq.Complex
import Monlib.Preq.Dite
import Monlib.Preq.Equiv
import Monlib.Preq.Finset
import Monlib.Preq.RCLikeLe
import Monlib.Preq.Ites
import Monlib.Preq.StarAlgEquiv

import Monlib.QuantumGraph.Basic
import Monlib.QuantumGraph.Example
import Monlib.QuantumGraph.PiMat
import Monlib.QuantumGraph.OfClassicalGraph
import Monlib.QuantumGraph.Degree
import Monlib.QuantumGraph.Grad
import Monlib.QuantumGraph.PiMatFinTwo
import Monlib.QuantumGraph.Matrix
-- import Monlib.QuantumGraph.Iso
-- import Monlib.QuantumGraph.Mess
-- import Monlib.QuantumGraph.Nontracial
-- import Monlib.QuantumGraph.QamA
-- import Monlib.QuantumGraph.QamAExample
-- import Monlib.QuantumGraph.ToProjections

import Monlib.RepTheory.AutMat

import Monlib.LinearAlgebra.Ips.Basic
-- import Monlib.LinearAlgebra.Ips.Frob
import Monlib.LinearAlgebra.Ips.Functional
import Monlib.LinearAlgebra.Ips.Ips
import Monlib.LinearAlgebra.Ips.MatIps
import Monlib.LinearAlgebra.Ips.MinimalProj
import Monlib.LinearAlgebra.Ips.MulOp
-- import Monlib.LinearAlgebra.Ips.Nontracial
import Monlib.LinearAlgebra.Ips.OpUnop
import Monlib.LinearAlgebra.Ips.Pos
import Monlib.LinearAlgebra.Ips.RankOne
import Monlib.LinearAlgebra.Ips.Strict
import Monlib.LinearAlgebra.Ips.Symm
import Monlib.LinearAlgebra.Ips.TensorHilbert
import Monlib.LinearAlgebra.Ips.Vn

import Monlib.LinearAlgebra.Matrix.Basic
import Monlib.LinearAlgebra.Matrix.Conj
import Monlib.LinearAlgebra.Matrix.IncludeBlock
import Monlib.LinearAlgebra.Matrix.IsAlmostHermitian
import Monlib.LinearAlgebra.Matrix.PosDefRpow
import Monlib.LinearAlgebra.Matrix.PosEqLinearMapIsPositive
import Monlib.LinearAlgebra.Matrix.Reshape
import Monlib.LinearAlgebra.Matrix.Spectra
import Monlib.LinearAlgebra.Matrix.StarOrderedRing
import Monlib.LinearAlgebra.Matrix.Cast

import Monlib.LinearAlgebra.Coalgebra.Lemmas
import Monlib.LinearAlgebra.Coalgebra.FiniteDimensional
import Monlib.LinearAlgebra.Coalgebra.MulOpposite

import Monlib.LinearAlgebra.TensorProduct.BasicLemmas
import Monlib.LinearAlgebra.TensorProduct.Lemmas
import Monlib.LinearAlgebra.TensorProduct.FiniteDimensional
import Monlib.LinearAlgebra.TensorProduct.OrthonormalBasis
import Monlib.LinearAlgebra.TensorProduct.Submodule

import Monlib.LinearAlgebra.QuantumSet.TensorProduct
import Monlib.LinearAlgebra.QuantumSet.Pi
import Monlib.LinearAlgebra.QuantumSet.Basic
import Monlib.LinearAlgebra.QuantumSet.SchurMul
import Monlib.LinearAlgebra.QuantumSet.Symm
import Monlib.LinearAlgebra.QuantumSet.Instances
import Monlib.LinearAlgebra.QuantumSet.QIso
import Monlib.LinearAlgebra.QuantumSet.PhiMap
import Monlib.LinearAlgebra.QuantumSet.DeltaForm
import Monlib.LinearAlgebra.QuantumSet.Subset
import Monlib.LinearAlgebra.QuantumSet.schurMulTensor