=== MMFLM86ModeLawAll.lean (507 lines)
  126: def AnchorModeComm (E : CentralExtension F L) (a b c : L) (j : ℕ) (r : ℕ) : Prop :=
  298: theorem actionFamily_modeVL_of_sumWindow (hs : ∀ a b : L, form a b = form b a)
  413: def AnchorModeCommStep (E : CentralExtension F L) : Prop :=
=== MMFLM86ModeLawAllAux.lean (633 lines)
   91: theorem factorial_smul_zsmul (m : ℕ) (Z : ℤ) (T : Module.End F (VL F L)) :
  147: theorem modeVL_smul_factor_sub (c : L) {r : ℕ} (t : F) (B : Module.End F (VL F L))
  162: theorem splitMinus_factorFamilyZero_eq (a : L) {n : ℕ} (hn : 1 ≤ n) (i : ℤ) (hi : 0 ≤ i) :
  191: theorem splitPlus_factorFamilyZero_eq (a : L) {n : ℕ} (hn : 1 ≤ n) (k : ℕ) :
  218: theorem splitPlus_factorFamilyZero_modeVL_sub (hs : ∀ a b : L, form a b = form b a)
  315: theorem headWindow_factorFamilyZero_modeVL_sub (a : L) {n : ℕ} (hn : 1 ≤ n) {r : ℕ} (hr : 1 ≤ r)
  350: theorem headWindow_factorFamilyZero_modeVL_shift (a : L) {n : ℕ} (hn : 1 ≤ n) {r : ℕ} (hr : 1 ≤ r)
  377: theorem tailWindow_factorFamilyZero_modeVL_sub (a : L) {n : ℕ} (hn : 1 ≤ n) {r : ℕ} (hr : 1 ≤ r)
  402: theorem tailWindow_factorFamilyZero_modeVL_shift (hs : ∀ a b : L, form a b = form b a)
  464: theorem actionFamily_modeVL_of_window (hs : ∀ a b : L, form a b = form b a)
  556: theorem actionFamily_factorFactorZero_modeVL (hs : ∀ a b : L, form a b = form b a)
=== MMFLM86ModeLawAllStep.lean (571 lines)
  134: theorem modeCommFam_step (hs : ∀ a b : L, form a b = form b a) (a b c : L) {r : ℕ} (hr : 1 ≤ r)
=== MMFLM86ModeLaw.lean MISSING
=== MMFLM86ModeLawAux.lean MISSING
=== MMFLM85PrescriptionCoeff.lean (244 lines)
=== MMFLM86ZOneFockOne.lean (960 lines)
  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)
  362: theorem diagSumWeighted_modeVL (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)
  457: theorem headWindow_modeVL_shift (a : L) {r : ℕ} (hr : 1 ≤ r) (c : L)
  481: theorem tailWindow_modeVL_shift (hs : ∀ a b : L, form a b = form b a) (a c : L) {r : ℕ}
  522: theorem actionFamily_modeVL (hs : ∀ a b : L, form a b = form b a) (E : CentralExtension F L)
  721: theorem ZAligned_modeVL (hs : ∀ a b : L, form a b = form b a) (E : CentralExtension F L)
  833: theorem zOneLineAt_modeVL_iotaVL (hs : ∀ a b : L, form a b = form b a) (E : CentralExtension F L)
=== MMFLM86MLA.lean MISSING
=== MMFLM86AnchorMode.lean MISSING
