OAI/NumberTheory/Ostmann/Arithmetic/CompensationEqualityPatterns.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.value_eq_of_rel line 13
  2. def OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.collapse line 18
  3. theorem OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.collapse_label line 29
  4. def OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.fiberEquiv line 33
  5. theorem OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.sum_eq_patterns line 47
  6. abbrev OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.Fiber line 56
  7. instance OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.fiberFintype line 58
  8. def OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.multiplicity line 61
  9. theorem OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.fiber_nonempty line 64
  10. theorem OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.multiplicity_pos line 69
  11. def OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.blockWeight line 73
  12. theorem OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.product_weights_by_blocks line 77
  13. theorem OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.product_by_multiplicity line 88
  14. theorem OAI.Ostmann.Arithmetic.CompensationEqualityPatterns.product_weighted_sum_eq_patterns line 95