OAI/NumberTheory/SiegelZeros/Differentials/DerivativeMatrix.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SiegelZeros.WeightedTorusJets.W28.MonomialBox line 16
2. def OAI.SiegelZeros.WeightedTorusJets.W28.boxExponent line 18
3. theorem OAI.SiegelZeros.WeightedTorusJets.W28.boxExponent_injective line 21
4. def OAI.SiegelZeros.WeightedTorusJets.W28.coefficientPolynomial line 28
5. theorem OAI.SiegelZeros.WeightedTorusJets.W28.coefficientPolynomial_coeff line 32
6. theorem OAI.SiegelZeros.WeightedTorusJets.W28.coefficientPolynomial_eq_zero_iff line 38
7. def OAI.SiegelZeros.WeightedTorusJets.W28.derivativeMatrix line 51
8. theorem OAI.SiegelZeros.WeightedTorusJets.W28.derivativeMatrix_eq_actual_jet line 57
9. theorem OAI.SiegelZeros.WeightedTorusJets.W28.derivativeMatrix_mulVec_eq_actual_jet line 65
10. theorem OAI.SiegelZeros.WeightedTorusJets.W28.actual_jet_annihilation_iff_rowSpan line 74
11. theorem OAI.SiegelZeros.WeightedTorusJets.W28.derivative_rows_span_of_annihilation line 96