OAI/NumberTheory/Jacobsthal/Siegel/NormalizedHomogeneousChartEquation.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Erdos970.WeightedTorusJets.Geometry.normalizedHomogeneousChartEquationline 19 - theorem
OAI.Erdos970.WeightedTorusJets.Geometry.affineProjChartMap_normalizedHomogeneousChartEquationline 26 - def
OAI.Erdos970.WeightedTorusJets.Geometry.projectiveStalkPolynomialEquivline 40 - def
OAI.Erdos970.WeightedTorusJets.Geometry.normalizedHomogeneousStalkEquationline 47 - theorem
OAI.Erdos970.WeightedTorusJets.Geometry.projectiveStalkPolynomialEquiv_normalizedEquationline 53 - theorem
OAI.Erdos970.WeightedTorusJets.Geometry.projectiveStalk_normalized_parameter_idealline 64