OAI/Analysis/Kaplansky/Regular/SlotEstimates.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KaplanskyConsequences.Regular.small_row_norm line 17
2. lemma OAI.KaplanskyConsequences.Regular.small_entry_gram_norm line 26
3. lemma OAI.KaplanskyConsequences.Regular.creationSum_small_defect line 35
4. lemma OAI.KaplanskyConsequences.Regular.creationSum_norm_le_two line 45
5. lemma OAI.KaplanskyConsequences.Regular.annihilationSum_norm_le line 60
6. lemma OAI.KaplanskyConsequences.Regular.small_gram_perturbation line 83
7. lemma OAI.KaplanskyConsequences.Regular.free_rows_near_gram line 103