OAI/Algebra/FinitisticAsymmetry/Triangular/Augmentation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LittleFinitistic.CummingsConstruction.mem_ker_augmentation line 17
2. def OAI.LittleFinitistic.CummingsConstruction.pureOldRadical line 27
3. lemma OAI.LittleFinitistic.CummingsConstruction.ker_square_pureOldRadical line 42
4. lemma OAI.LittleFinitistic.CummingsConstruction.pow_le_comap_pow_noncomm line 58
5. lemma OAI.LittleFinitistic.CummingsConstruction.augmentation_ker_nilpotent line 70
6. lemma OAI.LittleFinitistic.CummingsConstruction.left_dimensions_zero line 94