Documentation

LeanPool.Monlib4.LinearAlgebra

Imports

Init
LeanPool.Monlib4.LinearAlgebra.Coalgebra
LeanPool.Monlib4.LinearAlgebra.DirectSumFromTo
LeanPool.Monlib4.LinearAlgebra.End
LeanPool.Monlib4.LinearAlgebra.InnerAut
LeanPool.Monlib4.LinearAlgebra.InvariantSubmodule
LeanPool.Monlib4.LinearAlgebra.Ips
LeanPool.Monlib4.LinearAlgebra.IsProjPrime
LeanPool.Monlib4.LinearAlgebra.IsReal
LeanPool.Monlib4.LinearAlgebra.KroneckerToTensor
LeanPool.Monlib4.LinearAlgebra.LinearMapOp
LeanPool.Monlib4.LinearAlgebra.LmulRmul
LeanPool.Monlib4.LinearAlgebra.Matrix
LeanPool.Monlib4.LinearAlgebra.MulPrimePrime
LeanPool.Monlib4.LinearAlgebra.MyBimodule
LeanPool.Monlib4.LinearAlgebra.MySpec
LeanPool.Monlib4.LinearAlgebra.Nacgor
LeanPool.Monlib4.LinearAlgebra.OfNorm
LeanPool.Monlib4.LinearAlgebra.PiDirectSum
LeanPool.Monlib4.LinearAlgebra.PiStarOrderedRing
LeanPool.Monlib4.LinearAlgebra.PosMapIsReal
LeanPool.Monlib4.LinearAlgebra.QuantumSet
LeanPool.Monlib4.LinearAlgebra.TensorProduct
LeanPool.Monlib4.LinearAlgebra.ToMatrixOfEquiv

Imported by

LinearAlgebra #

Import-only index for the LinearAlgebra directory of the monlib4 import.