OAI/Analysis/WeakInfiniteness/IdealSpan.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakPureInfiniteness.algebraicIdealSpan line 28
2. lemma OAI.WeakPureInfiniteness.algebraicIdealSpan_mul_left line 32
3. lemma OAI.WeakPureInfiniteness.algebraicIdealSpan_mul_right line 43
4. lemma OAI.WeakPureInfiniteness.algebraicIdealSpan_star line 54
5. def OAI.WeakPureInfiniteness.algebraicIdealSubalgebra line 66
6. def OAI.WeakPureInfiniteness.generatedClosedIdeal line 71
7. instance OAI.WeakPureInfiniteness.(instance at line 74) line 74
8. instance OAI.WeakPureInfiniteness.(instance at line 77) line 77
9. lemma OAI.WeakPureInfiniteness.generatedClosedIdeal_mul_left line 81
10. lemma OAI.WeakPureInfiniteness.generatedClosedIdeal_mul_right line 89
11. lemma OAI.WeakPureInfiniteness.hereditary_le_generatedClosedIdeal line 96
12. lemma OAI.WeakPureInfiniteness.self_mem_generatedClosedIdeal line 107