OAI/Algebra/FormulaHitting/RationalTransfer.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NCHitting.jet line 17
  2. theorem OAI.NCHitting.jet_apply line 22
  3. def OAI.NCHitting.jetKernel line 28
  4. theorem OAI.NCHitting.mem_jetKernel line 31
  5. theorem OAI.NCHitting.jetKernel_antitone line 42
  6. theorem OAI.NCHitting.exists_independent_jet line 47
  7. theorem OAI.NCHitting.rational_series_independent line 69
  8. theorem OAI.NCHitting.rational_minor_ne_zero line 80
  9. theorem OAI.NCHitting.independent_of_rational_minor line 87