OAI/Analysis/WeakInfiniteness/FourColumnNorm.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPureInfiniteness.norm_rectangular_sqrt_left line 34
2. lemma OAI.WeakPureInfiniteness.norm_rectangular_sqrt_right line 52
3. lemma OAI.WeakPureInfiniteness.norm_rectangular_range_roots line 65
4. lemma OAI.WeakPureInfiniteness.norm_matrix_le_sum_entries line 74