OAI/NumberTheory/SiegelZeros/LocalAlgebra/DegreeSliceQuotientEquiv.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SiegelZeros.WeightedTorusJets.isRegular_generators_of_contains_regular_sequence line 68
2. theorem OAI.SiegelZeros.WeightedTorusJets.homogeneousMonomialBasis_repr line 164
3. theorem OAI.SiegelZeros.WeightedTorusJets.toMatrix_linearCombination_homogeneous line 169
4. def OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.degreeSliceQuotientEquiv line 189
5. def OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.cokernelEquivDegreePiece line 196
6. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.homogeneousComponent_mul_of_left_homogeneous line 275
7. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.homogeneousComponent_mul_of_right_homogeneous line 286
8. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.homogeneousComponent_mul_eq_zero_of_lt line 292