OAI/Algebra/OddKaplansky/GreedyColumns.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.OddKaplansky.GreedyColumns.Selectedline 16 - abbrev
OAI.OddKaplansky.GreedyColumns.Indexline 17 - instance
OAI.OddKaplansky.GreedyColumns.(instance at line 18)line 18 - lemma
OAI.OddKaplansky.GreedyColumns.independentline 20 - lemma
OAI.OddKaplansky.GreedyColumns.span_selectedline 37