OAI/Topology/ArtinGroups/Cancellation/Retained.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.Retained line 13
  2. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.retained_sum line 15
  3. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.reducedDifferential line 32
  4. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.reducedDifferential_entries line 35
  5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.reducedDifferential_degree line 39
  6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.reducedDifferential_square line 43
  7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.reducedDifferential_source_row line 47
  8. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.reducedDifferential_target_column line 51
  9. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.remainder_mul_reduced line 57
  10. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.reduced_mul_remainder line 61
  11. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.reduced line 65
  12. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.reductionMap line 80
  13. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.inclusionMap line 95
  14. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.reduction_inclusion line 109
  15. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.inclusion_reduction line 117
  16. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.reductionEquivalence line 132
  17. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.retained_card_lt line 147