OAI/NumberTheory/Jacobsthal/Siegel/FinrankSpanAlgebraMapImage.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Erdos970.WeightedTorusJets.Geometry.finrank_span_algebraMap_imageline 17 - theorem
OAI.Erdos970.WeightedTorusJets.Geometry.eval_source_jet_monomial_eq_map_rowline 35 - theorem
OAI.Erdos970.WeightedTorusJets.Geometry.finrank_span_source_jet_rows_eqline 47 - theorem
OAI.Erdos970.WeightedTorusJets.greedyPivots_eq_global_retained_setline 79