=== Definitions/MMFLM86SpineGap.lean
  173: def Theorem861SourceStatement (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ)
  308: abbrev VL (F : Type*) [Field F] (L : Type*) [AddCommGroup L] := FLMLattice.VL F L
  311: abbrev EndVL (F : Type*) [Field F] (L : Type*) [AddCommGroup L] := VL F L →ₗ[F] VL F L
  315: abbrev Op861 (F : Type*) [Field F] (L : Type*) [AddCommGroup L] :=
  327: theorem mul_smul_id_end (T : M →ₗ[F] M) (c : F) : T * (c • LinearMap.id) = c • T := by
  332: theorem smul_mul_end (c : F) (T D : M →ₗ[F] M) : (c • T) * D = c • (T * D) := by
  337: theorem mul_smul_end (c : F) (T D : M →ₗ[F] M) : T * (c • D) = c • (T * D) := by
  345: theorem smul_sub_end (c : F) (T D : M →ₗ[F] M) : c • (T - D) = c • T - c • D := by
  351: theorem commutator_end_smul_left (c : F) (A D : M →ₗ[F] M) :
  356: theorem commutator_end_smul_right (c : F) (A D : M →ₗ[F] M) :
  402: theorem mul_sourceDeltaExp861_eq (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ) (a : L) (i : ℕ) (m : ℤ)
  416: theorem sourceResidue861_eq_unshifted (Y : Op861 F L) (u v : VL F L)
  426: theorem sourceResidue861Unshifted_eq_corollary851Residue (Y : Op861 F L) (u v : VL F L) (K : ℕ)
  434: theorem sourceResidue861_eq_of_iterate_eq_zero (Y : Op861 F L) (u v : VL F L)
  466: def Theorem861SourceStatement (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ)
  481: def Theorem861SourceUnshiftedStatement (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ)
  495: theorem theorem861SourceStatement_iff_unshifted (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ)
  509: theorem theorem861SourceStatement_of_cutoff (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ)
  532: theorem commutatorFamily_add_left (Y : Op861 F L) (u u' v : VL F L) (m n : ℤ) :
  540: theorem commutatorFamily_smul_left (Y : Op861 F L) (c : F) (u v : VL F L) (m n : ℤ) :
  547: theorem commutatorFamily_add_right (Y : Op861 F L) (u v v' : VL F L) (m n : ℤ) :
  555: theorem commutatorFamily_smul_right (Y : Op861 F L) (c : F) (u v : VL F L) (m n : ℤ) :
  562: theorem commutatorFamily_zero_left (Y : Op861 F L) (v : VL F L) (m n : ℤ) :
  569: theorem commutatorFamily_zero_right (Y : Op861 F L) (u : VL F L) (m n : ℤ) :
  577: theorem sourceResidue861_add_left (Y : Op861 F L) (u u' v : VL F L)
  587: theorem sourceResidue861_smul_left (Y : Op861 F L) (c : F) (u v : VL F L)
  596: theorem sourceResidue861_add_right (Y : Op861 F L) (u v v' : VL F L)
  606: theorem sourceResidue861_smul_right (Y : Op861 F L) (c : F) (u v : VL F L)
  615: theorem sourceResidue861_zero_left (Y : Op861 F L) (v : VL F L) (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ)
  620: theorem sourceResidue861_zero_right (Y : Op861 F L) (u : VL F L) (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ)
  632: theorem theorem861Source_of_coeffFamily_and_spanning (Y : Op861 F L)
  683: theorem theorem861SourceStatement_zero_window_zero_state (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ)
  693: theorem span_range_id_eq_top :

=== Definitions/MMFLM810Theorem861Aligned.lean
  132: def Source861Aligned (C : EvenCocycle L form) (h2 : (2 : F) ≠ 0) (u' v' : FLMFock.M1 F L)
  138: def Display861Aligned (C : EvenCocycle L form) (h2 : (2 : F) ≠ 0) (u' v' : FLMFock.M1 F L)
  143: theorem source861Aligned_iff_display (C : EvenCocycle L form) (h2 : (2 : F) ≠ 0)
  152: theorem source861Aligned_iff_core (C : EvenCocycle L form) (h2 : (2 : F) ≠ 0)
  166: def Residue861Aligned (C : EvenCocycle L form) (h2 : (2 : F) ≠ 0) (u' v' : FLMFock.M1 F L)
  173: def Residual861Aligned (C : EvenCocycle L form) (h2 : (2 : F) ≠ 0) (u' v' : FLMFock.M1 F L)
  179: theorem display861Aligned_iff_residue (C : EvenCocycle L form) (h2 : (2 : F) ≠ 0)
  191: theorem residue861Aligned_iff_residual (C : EvenCocycle L form) (h2 : (2 : F) ≠ 0)
  199: theorem source861Aligned_iff_residual (C : EvenCocycle L form) (h2 : (2 : F) ≠ 0)
  208: theorem source861Aligned_of_residual (C : EvenCocycle L form) (h2 : (2 : F) ≠ 0)
  215: theorem residual_of_source861Aligned (C : EvenCocycle L form) (h2 : (2 : F) ≠ 0)
  227: theorem commutator_aligned_iotaVL (E : CentralExtension F L) (a b : L) (m n : ℤ) :
  239: theorem source861Aligned_iotaVL_of_nonneg (C : EvenCocycle L form) (h2 : (2 : F) ≠ 0)
  253: theorem toVertexOp_zAligned (E : CentralExtension F L) :
  259: theorem source861Aligned_of_jacobiIdentity (C : EvenCocycle L form) (h2 : (2 : F) ≠ 0)
  272: theorem source861Aligned_vectorwise (C : EvenCocycle L form) (h2 : (2 : F) ≠ 0)

=== Definitions/MMFLM86SourceBridge.lean
  112: theorem corollary851_iff_sourceUnshifted (Y : FLM86SG.Op861 F L) (u v : VL F L) (K : ℕ) :
  122: theorem corollary851_iff_sourceStatement (Y : FLM86SG.Op861 F L) (u v : VL F L) (a : L) (K : ℕ) :
  139: theorem corollary851_iff_theorem861SourceStatement {E : CentralExtension F L}
  158: theorem displayAtPair_iff_forall_theorem861SourceStatement {E : CentralExtension F L}
  181: theorem displayAllStates_iff_sourceStatements_of_evenCocycle (C : EvenCocycle L form)

=== Definitions/MMFLM86TheoremDisplay.lean
  109: def displayLeft863 (Y : FLM86SG.Op861 F L) (u v : FLM86SG.VL F L) :
  119: def displayRight863 (Y : FLM86SG.Op861 F L) (u v : FLM86SG.VL F L)
  127: def displayRight863Unshifted (Y : FLM86SG.Op861 F L) (u v : FLM86SG.VL F L) (K : ℕ) :
  133: theorem displayLeft863_apply (Y : FLM86SG.Op861 F L) (u v : FLM86SG.VL F L) (m n : ℤ) :
  138: theorem displayRight863_apply (Y : FLM86SG.Op861 F L) (u v : FLM86SG.VL F L)
  144: theorem displayRight863Unshifted_apply (Y : FLM86SG.Op861 F L) (u v : FLM86SG.VL F L) (K : ℕ)
  153: def Display863 (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ) (E : FLMLattice.CentralExtension F L)
  163: def Display863Unshifted (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ) (E : FLMLattice.CentralExtension F L)
  173: theorem display863_iff_sourceStatement (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ)
  185: theorem display863Unshifted_iff_sourceUnshiftedStatement (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ)
  202: theorem display863_iff_unshifted (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ)
  213: theorem display863_zero_state (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ)
  238: def Residue863 (Y : FLM86SG.Op861 F L) (u' v' : FLMFock.M1 F L) (a b : L) (K : ℕ) : Prop :=
  246: theorem deltaLeft_neg_one_eq_crossBracket_zero (Y : FLM86SG.Op861 F L) (u v : FLM86SG.VL F L)
  253: theorem deltaRight_neg_one_eq_crossIterate_zero (Y : FLM86SG.Op861 F L) (u v : FLM86SG.VL F L)
  262: theorem deltaRight_neg_one_eq_sourceResidue (Y : FLM86SG.Op861 F L) (u v : FLM86SG.VL F L)
  276: theorem display863_iff_residue863 (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ)
  305: theorem residue863_iff_corollary851 (Y : FLM86SG.Op861 F L) (u' v' : FLMFock.M1 F L) (a b : L)
  325: theorem residue863_iff_deltaResidueFace (Y : FLM86SG.Op861 F L) (u' v' : FLMFock.M1 F L)
  349: theorem residue863_of_jacobiIdentity (Y : FLM86SG.Op861 F L) (u' v' : FLMFock.M1 F L) (a b : L)
  360: theorem display863_of_jacobiIdentity (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ)
  371: theorem display863_of_jacobiDelta (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ)
  386: theorem residue863Vectorwise_of_jacobiAxiom (Y : FLM86SG.Op861 F L)
  406: theorem display863Vectorwise_of_display863 (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ)

=== Definitions/MMFLM86DisplayVOASplit.lean
   80: def UniformBracketWindow (Y : FLM86SG.Op861 F L) (u v : FLM86SG.VL F L) : Prop :=
   89: theorem uniformBracketWindow_of_weight {V : Type*} [AddCommGroup V] [Module F V]
  102: theorem uniformBracketWindow_of_grading (S : FLM85.WeightGrading F (FLM86SG.VL F L))
  122: theorem residue863_of_faithfulJacobi
  147: theorem display863_of_faithfulJacobi_at
  164: theorem display863_of_faithfulJacobi
  186: theorem display863_fixed_window
  204: theorem display863_of_voa_self
  223: theorem display863_of_voa
  268: theorem display863_of_remainingFields (bL : Module.Basis κ ℤ L) (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ)

=== Definitions/MMFLM810Assembly.lean
  104: def FacesAtStates (E : CentralExtension F L) : Prop :=
  117: def FaceWindows (E : CentralExtension F L) : Prop :=
  124: def ZeroFaces (E : CentralExtension F L) : Prop :=
  137: def PositiveFaces (E : CentralExtension F L) : Prop :=
  150: def NegativeFaces (E : CentralExtension F L) : Prop :=
  163: def NegativeOnGenerators (E : CentralExtension F L) : Prop :=
  177: def NegativeResidual (E : CentralExtension F L) : Prop :=
  196: def GroundedZeroFace (E : CentralExtension F L) : Prop :=
  207: theorem jacobiEvenCocycle_iff_faces (C : EvenCocycle L form) (h2 : (2 : F) ≠ 0) :
  215: theorem faces_iff_split (E : CentralExtension F L) :
  236: theorem faceWindows_zAligned (E : CentralExtension F L) :
  252: theorem corollary851_iff_zeroFace (Y : VL F L →ₗ[F] CoefFamily F (VL F L)) (u v : VL F L) (K : ℕ) :
  269: theorem zeroFaces_of_groundedZeroFace (hg : GroundedZeroFace (F := F) bL form E) :
  298: theorem positiveFaces_of_groundedZeroFace (hg : GroundedZeroFace (F := F) bL form E)

=== Definitions/MMFLM810AssemblyGrounded.lean
   68: theorem iterateOf_eq_zero_of_mem_span {Y : VL F L →ₗ[F] CoefFamily F (VL F L)} {S T : Set (VL F L)}
  104: theorem groundedZeroFace_of_spanningEventual (E : CentralExtension F L)
  145: theorem stepCorrected_of_spanningEventual (hs : ∀ a b : L, form a b = form b a)

=== Definitions/MMFLM88Jacobi.lean
  228: def componentOf (Y : M →ₗ[F] CoefFamily F M) (n : ℤ) (u : M) : M →ₗ[F] M :=
  233: theorem componentOf_apply (Y : M →ₗ[F] CoefFamily F M) (n : ℤ) (u : M) :
  238: theorem componentOf_eq_component (Y : M →ₗ[F] CoefFamily F M) (n : ℤ) (u : M) :
  258: def crossTerm (Y : M →ₗ[F] CoefFamily F M) (a b : M) (l m n : ℤ) (i : ℕ) : M →ₗ[F] M :=
  265: def crossTermSwap (Y : M →ₗ[F] CoefFamily F M) (a b : M) (l m n : ℤ) (i : ℕ) : M →ₗ[F] M :=
  273: def crossBracket (Y : M →ₗ[F] CoefFamily F M) (a b : M) (N : ℕ) (l m n : ℤ) : M →ₗ[F] M :=
  278: theorem crossBracket_apply (Y : M →ₗ[F] CoefFamily F M) (a b : M) (N : ℕ) (l m n : ℤ) :
  289: def CrossWindow (Y : M →ₗ[F] CoefFamily F M) (a b : M) (N : ℕ) : Prop :=
  294: theorem crossBracket_eq_of_window {Y : M →ₗ[F] CoefFamily F M} {a b : M} {N : ℕ}
  314: theorem crossBracket_zero_eq_commutatorFamily (Y : M →ₗ[F] CoefFamily F M) (a b : M) {N : ℕ}
  348: def iterateComponent (Y : M →ₗ[F] CoefFamily F M) (a b : M) (s j : ℤ) : M →ₗ[F] M :=
  353: theorem iterateComponent_eq_iterateOf (Y : M →ₗ[F] CoefFamily F M) (a b : M) (s j : ℤ) :
  360: def crossIterate (Y : M →ₗ[F] CoefFamily F M) (a b : M) (N : ℕ) (l m n : ℤ) : M →ₗ[F] M :=
  368: theorem crossIterate_zero_eq_bracketSum (Y : M →ₗ[F] CoefFamily F M) (a b : M) (N : ℕ) (m n : ℤ) :
  401: def deltaLeft (Y : M →ₗ[F] CoefFamily F M) (a b : M) (N : ℕ) (p m n : ℤ) : M →ₗ[F] M :=
  411: theorem deltaLeft_eq_crossBracket (Y : M →ₗ[F] CoefFamily F M) (a b : M) (N : ℕ) (p m n : ℤ) :
  419: def deltaRight (Y : M →ₗ[F] CoefFamily F M) (a b : M) (N : ℕ) (p m n : ℤ) : M →ₗ[F] M :=
  428: theorem deltaRight_eq_crossIterate (Y : M →ₗ[F] CoefFamily F M) (a b : M) (N : ℕ) (p m n : ℤ) :
  451: def JacobiIdentity (Y : M →ₗ[F] CoefFamily F M) (a b : M) (N : ℕ) : Prop :=
  457: def JacobiDelta (Y : M →ₗ[F] CoefFamily F M) (a b : M) (N : ℕ) : Prop :=
  464: theorem jacobiIdentity_iff_delta (Y : M →ₗ[F] CoefFamily F M) (a b : M) (N : ℕ) :
  481: theorem res_z0_face {Y : M →ₗ[F] CoefFamily F M} {a b : M} {N : ℕ}
  491: theorem res_z1_face {Y : M →ₗ[F] CoefFamily F M} {a b : M} {N : ℕ}
  498: theorem res_z2_face {Y : M →ₗ[F] CoefFamily F M} {a b : M} {N : ℕ}
  520: theorem binomCoeff_one (m : ℤ) : binomCoeff (F := F) m 1 = (m : F) := by
  528: theorem componentBracket_of_jacobiIdentity (Y : M →ₗ[F] CoefFamily F M) (a b : M) {N : ℕ}
  540: theorem componentBracket_of_jacobiIdentity_grading (S : WeightGrading F M)
  553: theorem corollary854_of_jacobiIdentity_grading (S : WeightGrading F M)
  565: theorem corollary851_of_jacobiIdentity (Y : M →ₗ[F] CoefFamily F M) (a b : M) {N : ℕ}
  578: theorem jacobiIdentity_zero_face_of_corollary851 {Y : M →ₗ[F] CoefFamily F M} {a b : M} {N : ℕ}
  588: theorem corollary851_iff_jacobiIdentity_zero_face (Y : M →ₗ[F] CoefFamily F M) (a b : M) {N : ℕ}
  610: theorem corollary8818_of_jacobiIdentity (Y : M →ₗ[F] CoefFamily F M) (a b : M) {N : ℕ}
  649: theorem commutatorFamily_eq_zero_of_nonneg_of_jacobiIdentity (Y : M →ₗ[F] CoefFamily F M) (a b : M)
  659: theorem commutatorFamily_eq_component_of_pairing_neg_one_of_jacobiIdentity
  672: theorem commutatorFamily_eq_two_terms_of_pairing_neg_two
  698: theorem commutatorFamily_eq_two_terms_of_pairing_neg_two_of_jacobiIdentity

