OAI/NumberTheory/Ostmann/Arithmetic/CompensationEqualityPatternsBasic.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.Pattern line 12
  2. def OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.patternCode line 14
  3. theorem OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.patternCode_injective line 18
  4. instance OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.patternFintype line 25
  5. instance OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.patternDecidableEq line 28
  6. theorem OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.card_pattern_le line 30
  7. def OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.patternOf line 35
  8. theorem OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.patternOf_rel line 39
  9. abbrev OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.Block line 44
  10. instance OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.blockFintype line 46
  11. instance OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.blockDecidableEq line 47
  12. def OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.label line 49
  13. theorem OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.label_surjective line 52
  14. theorem OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.card_block_le line 56
  15. def OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.blockType line 60
  16. theorem OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.blockType_label line 64
  17. def OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.BlockDraw line 67
  18. instance OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.blockDrawFintype line 70
  19. def OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.expand line 74
  20. theorem OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.patternOf_expand line 78