OAI/NumberTheory/Ostmann/Construction/DiagonalBadPairInversionComponents.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Ostmann.Conclusion.inverse_rightComponent_eq_of_overlapline 8 - def
OAI.Ostmann.Conclusion.inverseOverlapMapline 18 - theorem
OAI.Ostmann.Conclusion.inverseOverlapMap_surjectiveline 28 - theorem
OAI.Ostmann.Conclusion.overlapComponent_card_symmline 36 - theorem
OAI.Ostmann.Conclusion.badArrangement_symm_iffline 48 - theorem
OAI.Ostmann.Conclusion.transferBadArrangement_symm_iffline 52