OAI/Computability/PerfectCompleteness/Foundations/DummyEliminationLemmas.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.DummyElimination.exists_factor line 37
  2. structure OAI.PerfectCompleteness.DummyElimination.Slice line 51
  3. def OAI.PerfectCompleteness.DummyElimination.Slice.IsLift line 69
  4. def OAI.PerfectCompleteness.DummyElimination.Slice.Projected line 74
  5. def OAI.PerfectCompleteness.DummyElimination.Slice.Homogeneous line 78
  6. theorem OAI.PerfectCompleteness.DummyElimination.Slice.IsLift.projected line 81
  7. theorem OAI.PerfectCompleteness.DummyElimination.Slice.exists_lift_iff line 88
  8. def OAI.PerfectCompleteness.DummyElimination.Slice.fiberEquivHomogeneous line 140
  9. theorem OAI.PerfectCompleteness.DummyElimination.Slice.fiber_card_eq line 186
  10. theorem OAI.PerfectCompleteness.DummyElimination.Slice.projected_fibers_card_eq line 192
  11. theorem OAI.PerfectCompleteness.DummyElimination.Slice.projected_iff_basis line 200
  12. theorem OAI.PerfectCompleteness.DummyElimination.Slice.projected_equation_count_le line 214
  13. def OAI.PerfectCompleteness.ExactRationalMultiplicity.commonDenominator line 234
  14. def OAI.PerfectCompleteness.ExactRationalMultiplicity.multiplicity line 237
  15. theorem OAI.PerfectCompleteness.ExactRationalMultiplicity.commonDenominator_pos line 240
  16. theorem OAI.PerfectCompleteness.ExactRationalMultiplicity.denominator_dvd line 245
  17. theorem OAI.PerfectCompleteness.ExactRationalMultiplicity.commonDenominator_of_isEmpty line 250
  18. theorem OAI.PerfectCompleteness.ExactRationalMultiplicity.multiplicity_cast line 255
  19. theorem OAI.PerfectCompleteness.ExactRationalMultiplicity.multiplicity_pos line 268
  20. theorem OAI.PerfectCompleteness.ExactRationalMultiplicity.multiplicity_sum line 275
  21. theorem OAI.PerfectCompleteness.ExactRationalMultiplicity.multiplicity_div line 284
  22. theorem OAI.PerfectCompleteness.ExactRationalMultiplicity.multiplicity_le_denominator line 292
  23. structure OAI.PerfectCompleteness.ExactRationalMultiplicity.Uniformization line 300
  24. def OAI.PerfectCompleteness.ExactRationalMultiplicity.build line 308
  25. theorem OAI.PerfectCompleteness.ExactRationalMultiplicity.build_denominator line 317
  26. theorem OAI.PerfectCompleteness.ExactRationalMultiplicity.build_count line 321
  27. def OAI.PerfectCompleteness.ExactSeedMultiplicity.factor line 337
  28. def OAI.PerfectCompleteness.ExactSeedMultiplicity.denominator line 339
  29. def OAI.PerfectCompleteness.ExactSeedMultiplicity.perSeed line 341
  30. theorem OAI.PerfectCompleteness.ExactSeedMultiplicity.factor_positive line 343
  31. theorem OAI.PerfectCompleteness.ExactSeedMultiplicity.denominator_positive line 345
  32. theorem OAI.PerfectCompleteness.ExactSeedMultiplicity.count_dvd_factor line 348
  33. theorem OAI.PerfectCompleteness.ExactSeedMultiplicity.seed_total line 351
  34. theorem OAI.PerfectCompleteness.ExactSeedMultiplicity.perSeed_positive line 358
  35. theorem OAI.PerfectCompleteness.ExactSeedMultiplicity.perSeed_cast line 364
  36. theorem OAI.PerfectCompleteness.ExactSeedMultiplicity.perSeed_ratio line 374
  37. abbrev OAI.PerfectCompleteness.ExactSeedMultiplicity.Seeded line 385
  38. def OAI.PerfectCompleteness.ExactSeedMultiplicity.multiplicity line 392
  39. theorem OAI.PerfectCompleteness.ExactSeedMultiplicity.multiplicity_positive line 398
  40. theorem OAI.PerfectCompleteness.ExactSeedMultiplicity.sum_multiplicity line 402
  41. theorem OAI.PerfectCompleteness.ExactSeedMultiplicity.multiplicity_ratio line 416
  42. theorem OAI.PerfectCompleteness.ExactSeedMultiplicity.multiplicity_ratio_of_base line 422
  43. theorem OAI.PerfectCompleteness.NonzeroAverage.card_subtype_ne_real line 441
  44. theorem OAI.PerfectCompleteness.NonzeroAverage.card_mul_expect_eq line 448
  45. theorem OAI.PerfectCompleteness.NonzeroAverage.card_mul_expect_eq_sub_one line 455
  46. theorem OAI.PerfectCompleteness.NonzeroAverage.expect_subtype_ne_le_expect_of_expect_le line 462
  47. theorem OAI.PerfectCompleteness.NonzeroAverage.expect_subtype_ne_le_expect line 472
  48. theorem OAI.PerfectCompleteness.NonzeroAverage.zero_card_mul_expect line 480
  49. theorem OAI.PerfectCompleteness.NonzeroAverage.nonzero_expect_le_expect line 486