OAI/NumberTheory/OrdinaryCorrelations/HighTrace/ZeroExpression.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.zeroExpression line 17
2. def OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.append line 21
3. def OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.neg line 26
4. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.eval_zero line 30
5. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.coefficient_zero line 31
6. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.support_zero line 33
7. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.eval_append line 35
8. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.coefficient_append line 41
9. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.eval_neg line 47
10. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.coefficient_neg line 50
11. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.support_neg line 59
12. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.support_append line 62
13. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.factors_append_le line 75
14. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.abs_coefficient_append_le line 83