OAI/NumberTheory/Ostmann/Characters/PivotProductFibersCount.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Ostmann.Characters.PivotProductFibers.PrimeTuple line 14
  2. def OAI.Ostmann.Characters.PivotProductFibers.tupleProduct line 16
  3. def OAI.Ostmann.Characters.PivotProductFibers.tupleList line 18
  4. def OAI.Ostmann.Characters.PivotProductFibers.productFiber line 20
  5. theorem OAI.Ostmann.Characters.PivotProductFibers.mem_productFiber line 23
  6. theorem OAI.Ostmann.Characters.PivotProductFibers.tupleProduct_pos line 27
  7. theorem OAI.Ostmann.Characters.PivotProductFibers.tupleList_injective line 30
  8. theorem OAI.Ostmann.Characters.PivotProductFibers.tupleList_perm_of_product_eq line 37
  9. theorem OAI.Ostmann.Characters.PivotProductFibers.productFiber_card_le line 52
  10. def OAI.Ostmann.Characters.PivotProductFibers.distinctProductFiber line 70
  11. theorem OAI.Ostmann.Characters.PivotProductFibers.distinctProductFiber_subset line 74
  12. theorem OAI.Ostmann.Characters.PivotProductFibers.distinctProductFiber_card_le line 77