### normOrdered2
   Definitions/MMFLM86BoundPerState.lean:597 ns=['MM', 'FLM86BPS'] | theorem cutRight_normOrdered2_rankOne_ne (K2 : ℤ) :
   Definitions/MMFLM86CoherentCreated.lean:157 ns=['MM', 'FLM86CCF'] | theorem coherentTerm_eq_ZAligned_normOrdered2 (E : CentralExtension F L) (a b : L) (j l i 
   Definitions/MMFLM86CoherentCreated.lean:177 ns=['MM', 'FLM86CCF'] | theorem coherentSum_eq_ZAligned_normOrdered2Sum (E : CentralExtension F L) (a b : L) (j l 
   Definitions/MMFLM86CoherentCreated.lean:197 ns=['MM', 'FLM86CCF'] | theorem coherentCreatedForm_iff_normOrdered2 (E : CentralExtension F L) :
### annihExp_mul_creationExpVL_eq_sum_of_subset
   Definitions/MMFLM84RatioWindowClose.lean:813 ns=['MM', 'FLM84RWC'] | theorem annihExp_mul_creationExpVL_eq_sum_of_subset (hs : ∀ a b : L, form a b = form b a)
### powerFam_nestedExp
   Definitions/MMFLM86Display866ThreeInsert.lean:74 ns=['MM', 'FLM86D866T'] | theorem powerFam_nestedExp (hs : ∀ a b : L, form a b = form b a) (a : L) (l : ℕ) (bs : Fin
### flatGeneratorValueZ_eq_sum_binomCoeff
   Definitions/MMFLM86FlatBinomialApply.lean:118 ns=['MM', 'FLM86FBA'] | theorem flatGeneratorValueZ_eq_sum_binomCoeff (E : CentralExtension F L) (a b c : L) (j : 
### coherentFieldNat_eq_ZAligned
   Definitions/MMFLM86ModeIntertwine.lean:167 ns=['MM', 'FLM86MI'] | theorem coherentFieldNat_eq_ZAligned (E : CentralExtension F L) (a : L) (w : VL F L) (k : 
### ZAligned_modeVL
   Definitions/MMFLM86Corollary851ModeStepAux.lean:273 ns=['MM', 'FLM86C851M'] | theorem ZAligned_modeVL_add (bL : Module.Basis κ ℤ L)
   Definitions/MMFLM86Corollary851ModeStepAux.lean:285 ns=['MM', 'FLM86C851M'] | theorem ZAligned_modeVL_smul (bL : Module.Basis κ ℤ L)
   Definitions/MMFLM86DerivDictionary.lean:150 ns=['MM', 'FLM86DD'] | theorem ZAligned_modeVL_neg_one (E : CentralExtension F L) (a : L) (u : VL F L) :
   Definitions/MMFLM86DerivDictionary.lean:173 ns=['MM', 'FLM86DD'] | theorem ZAligned_modeVL_neg_one_stateOfVL (E : CentralExtension F L) (D : StateDatum L) (a
### zAlignedGeneratorFlat
   Definitions/MMFLM86FlatBinomialApply.lean:143 ns=['MM', 'FLM86FBA'] | theorem zAlignedGeneratorFlat_eq_sum_binomCoeff (hs : ∀ a b : L, form a b = form b a)
   Definitions/MMFLM86GeneratorLineAll.lean:205 ns=['MM', 'FLM86GLA'] | theorem zLineGeneratorFlat_iff_zAlignedGeneratorFlat (E : CentralExtension F L) :
   Definitions/MMFLM86GeneratorLineAllClose.lean:166 ns=['MM', 'FLM86GLC'] | theorem zAlignedGeneratorFlat_of_le_two (hs : ∀ a b : L, form a b = form b a)
   Definitions/MMFLM86GeneratorLineAllClose.lean:198 ns=['MM', 'FLM86GLC'] | theorem zAlignedGeneratorFlat (hs : ∀ a b : L, form a b = form b a) (E : CentralExtension 
### derivDefect_comp_modeVL_sub
   Definitions/MMFLM810CreationCommute.lean:369 ns=['MM', 'FLM810CC'] | theorem derivDefect_comp_modeVL_sub (hs : ∀ a b : L, form a b = form b a)
### modeVL_comm_creationExpVL_neg
   Definitions/MMFLM84TwoVarProduct.lean:599 ns=['MM', 'FLM84TV'] | theorem modeVL_comm_creationExpVL_neg (hs : ∀ a b : L, form a b = form b a) (a b : L)
### creationExpVL_comm
   Definitions/MMFLM84TwoVarProduct.lean:624 ns=['MM', 'FLM84TV'] | theorem creationExpVL_comm (hs : ∀ a b : L, form a b = form b a) (a b : L) (i k : ℤ) :
   Definitions/MMFLMLatticeState.lean:341 ns=['MM', 'FLMLatSt'] | theorem creationExpVL_comm_actVL (E : CentralExtension F L) (a c : L) (m : ℤ) (x : VL F L)
### honestBlockCoeffJL_one_rankOne
   Definitions/MMFLM86Matching8625Aux.lean:261 ns=['MM', 'FLM86M8625'] | theorem honestBlockCoeffJL_one_rankOne :
### ZAligned_createdState
   Definitions/MMFLM86ModeIntertwine.lean:336 ns=['MM', 'FLM86MI'] | theorem ZAligned_createdState (hs : ∀ a b : L, form a b = form b a)
### honestNegPairingCoeff_at_generators_window
   Definitions/MMFLM86NegPairingCoeffAllAux.lean:155 ns=['MM', 'FLM86NPCA'] | theorem honestNegPairingCoeff_at_generators_window (hs : ∀ a b : L, form a b = form b a)
