OAI/Algebra/DepthFive/LowerOperators.lean
0 declarations, 0 contain sorry, 0 declared as axioms
Finite-dimensional, monomial, and path-action descriptions of normalized IMM operators.
This file declares nothing itself. It gathers the 14 imports below, so a file that imports it gets all of them.
Imports
- OAI.Algebra.DepthFive.OperatorMonomials
- OAI.Algebra.DepthFive.OperatorNaturality
- OAI.Algebra.DepthFive.BidegreeDimension
- OAI.Algebra.DepthFive.IntermediateDimension
- OAI.Algebra.DepthFive.FockPaths
- OAI.Algebra.DepthFive.ImmOperatorPaths
- OAI.Algebra.DepthFive.PathShifts
- OAI.Algebra.DepthFive.PairingShifts
- OAI.Algebra.DepthFive.RelaxedPaths
- OAI.Algebra.DepthFive.OperatorTraceBridge
- OAI.Algebra.DepthFive.FiniteOperator
- OAI.Algebra.DepthFive.OperatorExponentBidegree
- OAI.Algebra.DepthFive.FockBidegreeBasis
- OAI.Algebra.DepthFive.BidegreeNonempty