OAI/Analysis/Kaplansky/Regular/CStarEstimates.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KaplanskyConsequences.norm_sum_mul_le line 15
2. lemma OAI.KaplanskyConsequences.tuple_product_column line 24
3. lemma OAI.KaplanskyConsequences.tuple_product_row line 33
4. lemma OAI.KaplanskyConsequences.exists_small_row_tuple line 48