=== MMFLM86ZOneFockOne.lean | ns=['MM', 'FLM86ZOF']
  120: theorem annihPair2_modeVL_sub (hs : ∀ a b : L, form a b = form b a) (a b c : L) {r : ℕ}
  137: theorem modeVL_mul_creationPair2_comm (hs : ∀ a b : L, form a b = form b a) (a b c : L) {r : ℕ}
  149: theorem modeVL_mul_midBlock2_comm (E : CentralExtension F L) (a b c : L) {r : ℕ} (i k : ℤ) :
  161: theorem modeVL_convWith2_comm (hs : ∀ a b : L, form a b = form b a) (E : CentralExtension F L)
  198: theorem normOrdered2_modeVL_sub (hs : ∀ a b : L, form a b = form b a) (E : CentralExtension F L)
  443: theorem modeVL_genFam_sub (hs : ∀ a b : L, form a b = form b a) (E : CentralExtension F L)
=== MMFLM86NegPairingFacesAux.lean | ns=['MM', 'FLM86NPFA']
   94: def blockFirstIdx (j l : ℕ) (m p : ℤ) : ℤ := (j : ℤ) + (l : ℤ) - m - p - 1
   97: theorem blockFirstIdx_sub_shiftIdx (j l : ℕ) (m p q k : ℤ) :
=== MMFLM86NegPairingCoeffGeneral.lean | ns=['MM', 'FLM86NPGC']
   89: noncomputable def honestBlockCoeffJ (a b : L) (j : ℕ) (m Q : ℤ) : F :=
   95: theorem honestBlockCoeffJ_zero (a b : L) (m Q : ℤ) :
=== MMFLM86NegPairingNonvacAux.lean | ns=['MM', 'FLM86NPNA']
  149: noncomputable def blockOfShift (E : CentralExtension F L) (a b : L) (j l : ℕ) (m Q : ℤ) :
  156: noncomputable def blockCombination (E : CentralExtension F L) (a b : L) (j l : ℕ) (m : ℤ)
  161: theorem blockOfShift_apply (E : CentralExtension F L) (a b : L) (j l : ℕ) (m Q : ℤ) :
  184: theorem blockCombination_apply (E : CentralExtension F L) (a b : L) (j l : ℕ) (m : ℤ)
  203: theorem blockOfShift_iotaVL (E : CentralExtension F L) (a b c : L) (j l : ℕ) (m Q : ℤ) :
  215: theorem blockOfShift_iotaVL_eq_zero_of_lt_right (E : CentralExtension F L) (a b c : L)
  225: theorem blockOfShift_iotaVL_eq_zero_of_lt_left (E : CentralExtension F L) (a b c : L)
=== MMFLM86Matching8625Aux.lean | ns=['MM', 'FLM86M8625']
  233: noncomputable def honestBlockCoeffJL (a b : L) (j l : Nat) (m Q : Int) : F :=
  238: theorem honestBlockCoeffJL_zero (a b : L) (j : Nat) (m Q : Int) :
  261: theorem honestBlockCoeffJL_one_rankOne :
=== MMFLM86Matching8625.lean | ns=['MM', 'FLM86M8625']
=== MMFLM86NegPairingFaces.lean | ns=['MM', 'FLM86NPF']
=== MMFLM86NormOrder.lean MISSING
=== MMFLM86NormOrdered2.lean MISSING
=== MMFLM86NegPairingFockStep.lean | ns=['MM', 'FLM86NPFS']
  112: def FaceAtFamily (E : CentralExtension F L) (a b : L) (j : ℕ) (m : ℤ) (n : ℕ)
  136: def FockStep (E : CentralExtension F L) : Prop :=
=== MMFLM86M8625.lean MISSING
