OAI/Analysis/WeakInfiniteness/UnitizationTensor.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPureInfiniteness.spatialElementary_ne_zero line 34
2. lemma OAI.WeakPureInfiniteness.rightElementaryHom_injective line 59
3. lemma OAI.WeakPureInfiniteness.minimalTensor_closed_submodule line 66
4. lemma OAI.WeakPureInfiniteness.minimalMapLeft_right_commute line 84
5. lemma OAI.WeakPureInfiniteness.minimalMapRight_eq_zero_iff line 88