OAI/NumberTheory/Ostmann/Arithmetic/IntegerCellSupport.lean
9 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Ostmann.Arithmetic.IntegerCell.integerSupportline 9 - def
OAI.Ostmann.Arithmetic.IntegerCell.openSupportline 13 - theorem
OAI.Ostmann.Arithmetic.IntegerCell.mem_integerSupportline 16 - theorem
OAI.Ostmann.Arithmetic.IntegerCell.mem_openSupportline 31 - theorem
OAI.Ostmann.Arithmetic.IntegerCell.openSupport_subsetline 37 - theorem
OAI.Ostmann.Arithmetic.IntegerCell.support_sdiff_subsetline 44 - theorem
OAI.Ostmann.Arithmetic.IntegerCell.closed_endpoint_errorline 59 - theorem
OAI.Ostmann.Arithmetic.IntegerCell.openSupport_sumline 77 - def
OAI.Ostmann.Arithmetic.IntegerCell.integerResidueMassline 82