OAI/NumberTheory/SiegelZeros/Differentials/InvariantDerivation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SiegelZeros.WeightedTorusJets.W18.invariantDerivation line 17
2. def OAI.SiegelZeros.WeightedTorusJets.W18.eigenvalue line 21
3. theorem OAI.SiegelZeros.WeightedTorusJets.W18.invariantDerivation_apply line 24
4. theorem OAI.SiegelZeros.WeightedTorusJets.W18.invariantDerivation_monomial line 37
5. theorem OAI.SiegelZeros.WeightedTorusJets.W18.invariantDerivation_monomial_smul line 47
6. theorem OAI.SiegelZeros.WeightedTorusJets.W18.coeff_invariantDerivation line 51
7. theorem OAI.SiegelZeros.WeightedTorusJets.W18.support_invariantDerivation_subset line 64
8. def OAI.SiegelZeros.WeightedTorusJets.W18.InBox line 72
9. theorem OAI.SiegelZeros.WeightedTorusJets.W18.inBox_invariantDerivation line 75