OAI/Algebra/AffineCancellation/ReesDerivation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ComplexCancellation.Rees.uniform_clear line 11
  2. lemma OAI.ComplexCancellation.Rees.stable_of_generators line 18
  3. lemma OAI.ComplexCancellation.Rees.clear_annihilate line 37
  4. lemma OAI.ComplexCancellation.Rees.scaled_is_ln line 52
  5. lemma OAI.ComplexCancellation.Rees.scaled_fixes line 56
  6. lemma OAI.ComplexCancellation.Rees.restrict_stable line 67
  7. lemma OAI.ComplexCancellation.Rees.scaled_restriction line 75
  8. def OAI.ComplexCancellation.Rees.up line 98
  9. lemma OAI.ComplexCancellation.Rees.red_up line 99
  10. lemma OAI.ComplexCancellation.Rees.red_surjective line 104
  11. lemma OAI.ComplexCancellation.Rees.primitive_reduction line 108