OAI/NumberTheory/OrdinaryCorrelations/HighTrace/SquarefreeExpression.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression line 18
2. def OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.eval line 25
3. def OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.support line 27
4. def OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.linearCoeff line 29
5. def OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.constantTerm line 32
6. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.mem_support line 35
7. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.eval_affine line 38
8. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.eval_congr_on line 50
9. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.linearCoeff_congr_on line 60
10. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.constantTerm_congr_on line 74
11. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.eval_independent line 88
12. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.abs_eval_le line 94