OAI/NumberTheory/OrdinaryCorrelations/HighTrace/ExtFields.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.ext_fields line 17
2. def OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.relabel line 24
3. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.factors_relabel line 28
4. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.coefficient_relabel line 31
5. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.mem_relabel_factor line 34
6. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.support_relabel line 38
7. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.eval_relabel line 60
8. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.linearCoeff_relabel line 67
9. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.SquarefreeExpression.constant_relabel line 86