### def sourceResidue861   (1)
   Definitions/MMFLM86SpineGap.lean:383: noncomputable def sourceResidue861 (Y : Op861 F L) (u v : VL F L)
### def sourceResidue861Unshifted   (1)
   Definitions/MMFLM86SpineGap.lean:393: noncomputable def sourceResidue861Unshifted (Y : Op861 F L) (u v : VL F L) (K : ℕ) (m n : ℤ) :
### def Hypothesis861  (1)
   Definitions/MMFLM86Theorem.lean:95: def Hypothesis861 (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ) (E : FLMLattice.CentralExtension F L) (a b : L) : Prop :=
### def stateOf  (3)
   Definitions/MMFLM85StateInterface.lean:256: def stateOf (D : LatticeDatum (F := F) bL form E) : VL F L :=
   Definitions/MMFLM85Uniqueness.lean:399: def stateOfVL (bL : Module.Basis κ ℤ L) (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ) (D : StateDatum L) : VL F L :=
   Definitions/MMFLM86Theorem.lean:200: noncomputable def stateOf (u' : FLMFock.M1 F L) (a : L) : FLMLattice.VL F L :=
### def Corollary851  (19)
   Definitions/MMFLM85Corollary.lean:371: def Corollary851 (Y : M →ₗ[F] CoefFamily F M) (a b : M) (K : ℕ) : Prop :=
   Definitions/MMFLM85Extraction.lean:491: def Corollary851Extraction (Y : VertexOp F V) (a b : V) (N : ℕ) : Prop :=
   Definitions/MMFLM86Corollary851AllStates.lean:91: def Corollary851ModeStep (Y : VL F L →ₗ[F] CoefFamily F (VL F L)) (K : ℕ) : Prop :=
   Definitions/MMFLM86Corollary851ModeStep.lean:109: def Corollary851ModeStepLeft (bL : Module.Basis κ ℤ L)
   Definitions/MMFLM86Corollary851ModeStep.lean:118: def Corollary851ModeStepRight (bL : Module.Basis κ ℤ L)
### def iterateOf  (3)
   Definitions/MMFLM85Iterate.lean:195: def iterateOf (Y : M →ₗ[F] CoefFamily F M) (a b : M) : ℤ → ℤ → (M →ₗ[F] M) :=
   Definitions/MMFLM85Iterate.lean:285: def iterateOfLinearRight (Y : M →ₗ[F] CoefFamily F M) (a : M) :
   Definitions/MMFLM85Iterate.lean:292: def iterateOfLinearLeft (Y : M →ₗ[F] CoefFamily F M) (b : M) :
### structure EvenCocycle  (1)
   Definitions/MMFLMLatticeModule.lean:526: structure EvenCocycle (L : Type v) [AddCommGroup L] (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ) where
### def toCentralExtension  (1)
   Definitions/MMFLMLatticeModule.lean:550: def toCentralExtension (C : EvenCocycle L form) (h2 : (2 : F) ≠ 0) : CentralExtension F L where
### abbrev Op861  (1)
   Definitions/MMFLM86SpineGap.lean:315: abbrev Op861 (F : Type*) [Field F] (L : Type*) [AddCommGroup L] :=
### theorem display863_of_faithfulJacobi  (2)
   Definitions/MMFLM86DisplayVOASplit.lean:147: theorem display863_of_faithfulJacobi_at
   Definitions/MMFLM86DisplayVOASplit.lean:164: theorem display863_of_faithfulJacobi
### theorem display863_of_voa   (0)
### theorem display863_of_remainingFields  (1)
   Definitions/MMFLM86DisplayVOASplit.lean:268: theorem display863_of_remainingFields (bL : Module.Basis κ ℤ L) (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ)
### structure WeightGrading  (1)
   Definitions/MMFLM85Components.lean:166: structure WeightGrading (F : Type*) [Field F] (V : Type*) [AddCommGroup V] [Module F V] where
### def WeightGrading  (1)
   Definitions/MMFLM85Components.lean:281: def WeightGrading.IsHomogeneousOp (S : WeightGrading F V) (T : V →ₗ[F] V) (p : ℤ) : Prop :=
