OAI/NumberTheory/Jacobsthal/Siegel/TorusIntoProj.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Erdos970.WeightedTorusJets.Geometry.torusIntoProjline 18 - theorem
OAI.Erdos970.WeightedTorusJets.Geometry.torusIntoProj_applyline 26 - theorem
OAI.Erdos970.WeightedTorusJets.Geometry.closure_torusIntoProj_zeroLocus_eq_affineline 34 - theorem
OAI.Erdos970.WeightedTorusJets.Geometry.closure_torusIntoProj_zeroLocusline 53