OAI/NumberTheory/Catalan/Determinants/RawMinorCoefficientExpansion.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.InternalCatalan.rawCoefficientIndex line 14
  2. def OAI.InternalCatalan.rawCoefficientVector line 17
  3. def OAI.InternalCatalan.rawCoefficientScalar line 23
  4. def OAI.InternalCatalan.rawCoefficientMinor line 28
  5. theorem OAI.InternalCatalan.rawColumnTerm_coefficient_expansion line 35
  6. theorem OAI.InternalCatalan.rawColumnMinor_coefficient_expansion line 60
  7. theorem OAI.InternalCatalan.rawCoefficientMinor_eq_zero_of_repeat_exception line 95
  8. theorem OAI.InternalCatalan.rawCoefficientMinor_eq_zero_of_repeat_boundary line 106
  9. theorem OAI.InternalCatalan.rawCoefficientMinor_exception_injOn line 117
  10. theorem OAI.InternalCatalan.rawCoefficientMinor_boundary_injOn line 127
  11. theorem OAI.InternalCatalan.rawColumnMinor_coefficient_expansion_injective line 137