OAI/Analysis/Kaplansky/Regular/FreeEstimates.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KaplanskyConsequences.Regular.norm_disjoint_sum_le line 16
2. lemma OAI.KaplanskyConsequences.Regular.cutSum_norm_le line 31
3. lemma OAI.KaplanskyConsequences.Regular.sum_negative_norm_le line 52
4. lemma OAI.KaplanskyConsequences.Regular.diagonal_creation_commute line 59
5. lemma OAI.KaplanskyConsequences.Regular.diagonal_starCreation_commute line 64
6. lemma OAI.KaplanskyConsequences.Regular.coeff_creation_star_mul line 69
7. lemma OAI.KaplanskyConsequences.Regular.creationSum_star_mul line 76
8. lemma OAI.KaplanskyConsequences.Regular.creationSum_gram_self line 84
9. lemma OAI.KaplanskyConsequences.Regular.creationSum_gram_cross line 102