OAI/NumberTheory/Jacobsthal/Siegel/DegreeSliceQuotientEquiv.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.WeightedTorusJets.isRegular_generators_of_contains_regular_sequence line 39
2. theorem OAI.Erdos970.WeightedTorusJets.homogeneousMonomialBasis_repr line 71
3. theorem OAI.Erdos970.WeightedTorusJets.toMatrix_linearCombination_homogeneous line 76
4. def OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.degreeSliceQuotientEquiv line 96
5. def OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.cokernelEquivDegreePiece line 103
6. theorem OAI.Erdos970.WeightedTorusJets.Geometry.homogeneousComponent_mul_of_left_homogeneous line 128
7. theorem OAI.Erdos970.WeightedTorusJets.Geometry.homogeneousComponent_mul_of_right_homogeneous line 139
8. theorem OAI.Erdos970.WeightedTorusJets.Geometry.homogeneousComponent_mul_eq_zero_of_lt line 145