OAI/Algebra/FinitisticAsymmetry/Augmentation/SplitBasic.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LittleFinitistic.SplitBasic.pow_le_comap_pow line 12
  2. def OAI.LittleFinitistic.SplitBasic.squareZeroAugmentation line 29
  3. lemma OAI.LittleFinitistic.SplitBasic.squareZero_surjective line 31
  4. lemma OAI.LittleFinitistic.SplitBasic.squareZero_ker_nilpotent line 36
  5. def OAI.LittleFinitistic.SplitBasic.productAugmentation line 63
  6. lemma OAI.LittleFinitistic.SplitBasic.product_surjective line 70
  7. lemma OAI.LittleFinitistic.SplitBasic.product_ker_nilpotent line 78
  8. def OAI.LittleFinitistic.SplitBasic.oppositeAugmentation line 99
  9. lemma OAI.LittleFinitistic.SplitBasic.opposite_surjective line 106
  10. lemma OAI.LittleFinitistic.SplitBasic.unop_mem_pow_ker line 111
  11. lemma OAI.LittleFinitistic.SplitBasic.opposite_ker_nilpotent line 124