OAI/Analysis/WeakInfiniteness/TensorAbsorption.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.WeakPureInfiniteness.minimalTensor_separable line 34
2. lemma OAI.WeakPureInfiniteness.minimalElementary_eq_zero_iff line 69
3. def OAI.WeakPureInfiniteness.minimalLeftEmbedding line 112
4. lemma OAI.WeakPureInfiniteness.minimalLeftEmbedding_injective line 120
5. lemma OAI.WeakPureInfiniteness.minimalLeftEmbedding_isometry line 125