Documentation
LeanPool
.
Ado
.
Imports
Search
return to top
source
Imports
Init
LeanPool.Ado
LeanPool.Ado.LinearAlgebra.Determinant
LeanPool.Ado.LinearAlgebra.Projection
LeanPool.Ado.Order.CompactlyGenerated
LeanPool.Ado.Order.SupIndep
LeanPool.Ado.Algebra.DirectSum.Internal
LeanPool.Ado.Algebra.Lie.Basic
LeanPool.Ado.Algebra.Lie.CompleteReducibility
LeanPool.Ado.Algebra.Lie.DirectSum
LeanPool.Ado.Algebra.Lie.NilpotentExtension
LeanPool.Ado.Algebra.Lie.Nilradical
LeanPool.Ado.Algebra.Lie.OfAssociative
LeanPool.Ado.Algebra.Lie.Prod
LeanPool.Ado.Algebra.Lie.Quotient
LeanPool.Ado.Algebra.Ring.Subgroup
LeanPool.Ado.Algebra.WordFiltration.Basic
LeanPool.Ado.LinearAlgebra.BilinearForm.BaseChange
LeanPool.Ado.LinearAlgebra.BilinearForm.Multilinear
LeanPool.Ado.LinearAlgebra.Dimension.DirectSum
LeanPool.Ado.LinearAlgebra.Eigenspace.Semisimple
LeanPool.Ado.LinearAlgebra.Eigenspace.Separation
LeanPool.Ado.LinearAlgebra.End.Prod
LeanPool.Ado.LinearAlgebra.Multilinear.Span
LeanPool.Ado.LinearAlgebra.RootSystem.Chamber
LeanPool.Ado.LinearAlgebra.RootSystem.DominantCone
LeanPool.Ado.LinearAlgebra.RootSystem.DynkinType
LeanPool.Ado.LinearAlgebra.RootSystem.EquivInvariance
LeanPool.Ado.LinearAlgebra.RootSystem.Height
LeanPool.Ado.LinearAlgebra.RootSystem.Positive
LeanPool.Ado.LinearAlgebra.RootSystem.SimpleReflections
LeanPool.Ado.LinearAlgebra.TensorProduct.Decomposition
LeanPool.Ado.LinearAlgebra.TensorProduct.Kernel
LeanPool.Ado.LinearAlgebra.TensorProduct.Range
LeanPool.Ado.RepresentationTheory.Lie.Abelian
LeanPool.Ado.RepresentationTheory.Lie.CofiniteKernel
LeanPool.Ado.RingTheory.Ideal.Operations
LeanPool.Ado.RingTheory.SimpleModule.Basic
LeanPool.Ado.Algebra.Lie.BaseChange.Hom
LeanPool.Ado.Algebra.Lie.BaseChange.MaxTrivSubmodule
LeanPool.Ado.Algebra.Lie.BaseChange.Quotient
LeanPool.Ado.Algebra.Lie.BaseChange.Radical
LeanPool.Ado.Algebra.Lie.BaseChange.Range
LeanPool.Ado.Algebra.Lie.Derivation.Basic
LeanPool.Ado.Algebra.Lie.Derivation.Ideal
LeanPool.Ado.Algebra.Lie.Derivation.LocallyNilpotent
LeanPool.Ado.Algebra.Lie.Derivation.Quotient
LeanPool.Ado.Algebra.Lie.Derivation.Solvable
LeanPool.Ado.Algebra.Lie.GeneralLinear.Basic
LeanPool.Ado.Algebra.Lie.GeneralLinear.Finrank
LeanPool.Ado.Algebra.Lie.HighestWeight.Basic
LeanPool.Ado.Algebra.Lie.HighestWeight.Casimir
LeanPool.Ado.Algebra.Lie.HighestWeight.CompleteReducibility
LeanPool.Ado.Algebra.Lie.HighestWeight.Existence
LeanPool.Ado.Algebra.Lie.HighestWeight.Integrability
LeanPool.Ado.Algebra.Lie.HighestWeight.Integrable
LeanPool.Ado.Algebra.Lie.HighestWeight.Maximal
LeanPool.Ado.Algebra.Lie.HighestWeight.Module
LeanPool.Ado.Algebra.Lie.HighestWeight.Reflection
LeanPool.Ado.Algebra.Lie.HighestWeight.Separation
LeanPool.Ado.Algebra.Lie.HighestWeight.Trivial
LeanPool.Ado.Algebra.Lie.Killing.BaseChange
LeanPool.Ado.Algebra.Lie.Killing.Basic
LeanPool.Ado.Algebra.Lie.Killing.DualBasis
LeanPool.Ado.Algebra.Lie.Killing.Perfect
LeanPool.Ado.Algebra.Lie.Killing.Quotient
LeanPool.Ado.Algebra.Lie.LeviDecomposition.Abelian
LeanPool.Ado.Algebra.Lie.LeviDecomposition.Solvable
LeanPool.Ado.Algebra.Lie.SemiDirect.AdNilpotent
LeanPool.Ado.Algebra.Lie.SemiDirect.Basic
LeanPool.Ado.Algebra.Lie.Sl2.Basic
LeanPool.Ado.Algebra.Lie.Sl2.Casimir
LeanPool.Ado.Algebra.Lie.Sl2.Classification
LeanPool.Ado.Algebra.Lie.Sl2.CompleteReducibility
LeanPool.Ado.Algebra.Lie.Sl2.Decomposition
LeanPool.Ado.Algebra.Lie.Sl2.Spectrum
LeanPool.Ado.Algebra.Lie.Sl2.Standard
LeanPool.Ado.Algebra.Lie.Sl2.WeightMultiplicity
LeanPool.Ado.Algebra.Lie.Sl2.WeightString
LeanPool.Ado.Algebra.Lie.Solvable.Basic
LeanPool.Ado.Algebra.Lie.Solvable.Derived
LeanPool.Ado.Algebra.Lie.Subalgebra.Top
LeanPool.Ado.Algebra.Lie.Submodule.Atom
LeanPool.Ado.Algebra.Lie.Submodule.Decomposition
LeanPool.Ado.Algebra.Lie.Submodule.DirectSum
LeanPool.Ado.Algebra.Lie.Submodule.Finrank
LeanPool.Ado.Algebra.Lie.Submodule.LocallyFinite
LeanPool.Ado.Algebra.Lie.UniversalEnveloping.Basic
LeanPool.Ado.Algebra.Lie.UniversalEnveloping.Casimir
LeanPool.Ado.Algebra.Lie.UniversalEnveloping.CofiniteRefinement
LeanPool.Ado.Algebra.Lie.UniversalEnveloping.Functoriality
LeanPool.Ado.Algebra.Lie.UniversalEnveloping.LieIdeal
LeanPool.Ado.Algebra.Lie.UniversalEnveloping.Module
LeanPool.Ado.Algebra.Lie.Weights.Basic
LeanPool.Ado.Algebra.Lie.Weights.Borel
LeanPool.Ado.Algebra.Lie.Weights.Casimir
LeanPool.Ado.Algebra.Lie.Weights.Diagonalizable
LeanPool.Ado.Algebra.Lie.Weights.Eigenvector
LeanPool.Ado.Algebra.Lie.Weights.Exact
LeanPool.Ado.Algebra.Lie.Weights.FormalCharacter
LeanPool.Ado.Algebra.Lie.Weights.Integrable
LeanPool.Ado.Algebra.Lie.Weights.Integrality
LeanPool.Ado.Algebra.Lie.Weights.InvariantForm
LeanPool.Ado.Algebra.Lie.Weights.Killing
LeanPool.Ado.Algebra.Lie.Weights.Positivity
LeanPool.Ado.Algebra.Lie.Weights.Prod
LeanPool.Ado.Algebra.Lie.Weights.Projection
LeanPool.Ado.Algebra.Lie.Weights.Reflection
LeanPool.Ado.Algebra.Lie.Weights.Span
LeanPool.Ado.Algebra.Lie.Weights.String
LeanPool.Ado.Algebra.Lie.Weights.TensorProduct
LeanPool.Ado.Algebra.Lie.Weights.Trace
LeanPool.Ado.Algebra.Lie.Weights.WeylInvariance
LeanPool.Ado.LinearAlgebra.Matrix.PosDef.Basic
LeanPool.Ado.LinearAlgebra.RootSystem.FiniteType.Basic
LeanPool.Ado.LinearAlgebra.RootSystem.FiniteType.Bounded
LeanPool.Ado.LinearAlgebra.RootSystem.Weyl.Group
LeanPool.Ado.LinearAlgebra.RootSystem.Weyl.Vector
LeanPool.Ado.RepresentationTheory.Lie.Ado.CharacteristicZero
LeanPool.Ado.RepresentationTheory.Lie.EnvelopingExtension.Basic
LeanPool.Ado.RepresentationTheory.Lie.EnvelopingExtension.Nilpotent
LeanPool.Ado.RepresentationTheory.Lie.EnvelopingExtension.Nilrepresentation
LeanPool.Ado.RingTheory.Ideal.Quotient.Integral
LeanPool.Ado.RingTheory.Ideal.Quotient.Nilpotent
LeanPool.Ado.Algebra.Lie.HighestWeight.Weight.Support
LeanPool.Ado.Algebra.Lie.UniversalEnveloping.Derivation.Basic
LeanPool.Ado.Algebra.Lie.UniversalEnveloping.Derivation.Nilpotent
LeanPool.Ado.Algebra.Lie.UniversalEnveloping.PBW.Basic
LeanPool.Ado.Algebra.Lie.UniversalEnveloping.PBW.Cofinite
LeanPool.Ado.Algebra.Lie.UniversalEnveloping.PBW.Finite
LeanPool.Ado.Algebra.Lie.UniversalEnveloping.PBW.LeadingTerm
LeanPool.Ado.Algebra.Lie.UniversalEnveloping.PBW.Ordered
Imported by