OAI/NumberTheory/OrdinaryCorrelations/HighTrace/Restrict.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.restrict line 19
2. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.mem_restrict_factors line 23
3. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.mem_restrict_support line 26
4. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.prod_restrict line 34
5. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.eval_restrict line 44
6. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.prod_restrict_erase line 53
7. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.coefficient_restrict line 68
8. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.constant_restrict line 80
9. def OAI.OrdinaryCorrelations.ArithmeticSaving.TriangularExpressions.restrictEmbedding line 97
10. def OAI.OrdinaryCorrelations.ArithmeticSaving.TriangularExpressions.restrict line 101
11. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.TriangularExpressions.numericClause_restrict line 118
12. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.TriangularExpressions.admissible_restrict line 136