OAI/RingTheory/Multiplicity/RootTowerRootWeight.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Lech.RootTower.root_weight_mul line 14
  2. lemma OAI.Lech.NormalizedLength.length_span_le_baseChange line 32
  3. structure OAI.Lech.NormalizedLength.Tower line 47
  4. def OAI.Lech.NormalizedLength.Tower.stage line 74
  5. def OAI.Lech.NormalizedLength.Tower.finiteLength line 78
  6. def OAI.Lech.NormalizedLength.Tower.length line 81
  7. lemma OAI.Lech.NormalizedLength.Tower.span_mono_stage line 84
  8. lemma OAI.Lech.NormalizedLength.Tower.stage_antitone line 91
  9. lemma OAI.Lech.NormalizedLength.Tower.stage_mono line 113
  10. lemma OAI.Lech.NormalizedLength.Tower.finiteLength_mono line 120
  11. lemma OAI.Lech.NormalizedLength.Tower.finiteLength_le_stage line 123
  12. lemma OAI.Lech.NormalizedLength.Tower.finiteLength_le_length line 126
  13. lemma OAI.Lech.NormalizedLength.Tower.mem_span_iff_exists_stage line 128
  14. lemma OAI.Lech.NormalizedLength.Tower.finite_subset_span_stage line 149
  15. lemma OAI.Lech.NormalizedLength.Tower.finiteLength_le_of_span_le line 165
  16. lemma OAI.Lech.NormalizedLength.Tower.finiteLength_eq_of_span_eq line 182
  17. lemma OAI.Lech.NormalizedLength.Tower.stage_image_le line 187
  18. lemma OAI.Lech.NormalizedLength.Tower.stage_image_eq line 201
  19. lemma OAI.Lech.NormalizedLength.Tower.finiteLength_image_le line 211
  20. lemma OAI.Lech.NormalizedLength.Tower.finiteLength_image_eq line 215
  21. lemma OAI.Lech.NormalizedLength.Tower.length_le_of_injective line 220
  22. lemma OAI.Lech.NormalizedLength.Tower.length_le_of_surjective line 228
  23. lemma OAI.Lech.NormalizedLength.Tower.length_eq_of_equiv line 245
  24. lemma OAI.Lech.NormalizedLength.Tower.stage_zero line 249
  25. lemma OAI.Lech.NormalizedLength.Tower.length_zero line 252
  26. lemma OAI.Lech.NormalizedLength.Tower.length_eq_finiteLength_of_span_top line 255
  27. lemma OAI.Lech.NormalizedLength.Tower.stage_add_le line 264
  28. lemma OAI.Lech.NormalizedLength.Tower.finiteLength_add_le line 306
  29. lemma OAI.Lech.NormalizedLength.Tower.length_add_le line 316
  30. lemma OAI.Lech.NormalizedLength.Tower.stage_le_add_kernel line 335
  31. lemma OAI.Lech.NormalizedLength.Tower.finiteLength_le_length_of_subset line 411
  32. lemma OAI.Lech.NormalizedLength.Tower.finiteLength_le_length_kernel_add_stage line 426
  33. lemma OAI.Lech.NormalizedLength.Tower.length_le_kernel_add line 451
  34. theorem OAI.Lech.NormalizedLength.Tower.length_eq_kernel_add line 461
  35. lemma OAI.Lech.NormalizedLength.Tower.length_eq_add_of_exact line 466
  36. lemma OAI.Lech.NormalizedLength.Tower.length_prod line 473
  37. lemma OAI.Lech.NormalizedLength.Tower.length_sup_le line 487
  38. lemma OAI.Lech.NormalizedLength.Tower.finite_subset_directed line 502
  39. lemma OAI.Lech.NormalizedLength.Tower.length_eq_iSup_of_directed line 519
  40. lemma OAI.Lech.NormalizedLength.Tower.length_range_le line 530
  41. lemma OAI.Lech.NormalizedLength.Tower.length_directed_iSup line 533
  42. lemma OAI.Lech.NormalizedLength.Tower.length_bot line 550
  43. lemma OAI.Lech.NormalizedLength.Tower.length_top line 552
  44. theorem OAI.Lech.NormalizedLength.Tower.length_iSup_eq_zero line 556
  45. theorem OAI.Lech.NormalizedLength.Tower.length_directSum_eq_zero line 585
  46. theorem OAI.Lech.NormalizedLength.Tower.length_directLimit_eq_zero_of_tendsto line 606