OAI/NumberTheory/SiegelZeros/Determinants/NormalSurjectivity.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SiegelZeros.WeightedTorusJets.NormalExactness.normalRestriction line 15
2. theorem OAI.SiegelZeros.WeightedTorusJets.NormalExactness.normalRestriction_toCotangent line 27
3. theorem OAI.SiegelZeros.WeightedTorusJets.NormalExactness.normalRestriction_eq_zero_iff line 30
4. def OAI.SiegelZeros.WeightedTorusJets.NormalExactness.quotientDerivation line 40
5. theorem OAI.SiegelZeros.WeightedTorusJets.NormalExactness.quotientDerivation_mk line 52
6. def OAI.SiegelZeros.WeightedTorusJets.NormalExactness.tangentInclusion line 56
7. theorem OAI.SiegelZeros.WeightedTorusJets.NormalExactness.tangentInclusion_apply line 60
8. theorem OAI.SiegelZeros.WeightedTorusJets.NormalExactness.tangentInclusion_injective line 63
9. theorem OAI.SiegelZeros.WeightedTorusJets.NormalExactness.normalRestriction_kernel_eq_tangent_range line 69
10. theorem OAI.SiegelZeros.WeightedTorusJets.NormalExactness.normalRestriction_surjective line 83
11. theorem OAI.SiegelZeros.WeightedTorusJets.NormalExactness.torus_generic_normalRestriction_surjective line 102