OAI/Analysis/JiangSu/Nonunital/NonUnitalRoots.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Pureness.nonUnitalNormalize_nonneg line 15
2. lemma OAI.Pureness.nonUnitalNormalize_zero line 19
3. lemma OAI.Pureness.nonUnitalNormalize_norm_le line 23
4. lemma OAI.Pureness.nonUnitalNormalize_smul line 29
5. lemma OAI.Pureness.nonUnitalRoot_monotone line 35
6. lemma OAI.Pureness.nonUnital_nnrpow_map line 61
7. lemma OAI.Pureness.nonUnital_nnrpow_smul line 74