OAI/RingTheory/Multiplicity/FrobeniusIntermediatePowerMap.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Lech.FrobeniusIntermediate.powerMap line 25
  2. lemma OAI.Lech.FrobeniusIntermediate.powerMap_val line 28
  3. lemma OAI.Lech.FrobeniusIntermediate.inclusion_comp_powerMap line 30
  4. instance OAI.Lech.FrobeniusIntermediate.(instance at line 32) line 32
  5. lemma OAI.Lech.FrobeniusIntermediate.map_radical_primary line 38
  6. lemma OAI.Lech.FrobeniusIntermediate.mapped_ideal line 61
  7. instance OAI.Lech.FrobeniusIntermediate.(instance at line 66) line 66
  8. lemma OAI.Lech.FrobeniusIntermediate.inclusion_comp_iterateFrobenius line 68
  9. lemma OAI.Lech.FrobeniusIntermediate.map_frobenius_ideal line 74
  10. lemma OAI.Lech.FrobeniusIntermediate.quotient_length_eq line 94
  11. theorem OAI.Lech.FrobeniusIntermediate.exists_positive_rank_transfer line 107
  12. def OAI.Lech.SeparableOrder.order line 160
  13. lemma OAI.Lech.SeparableOrder.mem_order line 165
  14. instance OAI.Lech.SeparableOrder.orderFinite line 167
  15. def OAI.Lech.SeparableOrder.toField line 173
  16. lemma OAI.Lech.SeparableOrder.toField_injective line 184
  17. instance OAI.Lech.SeparableOrder.orderFieldAlgebra line 189
  18. instance OAI.Lech.SeparableOrder.orderFieldTower line 192
  19. instance OAI.Lech.SeparableOrder.orderFieldAmbientTower line 195
  20. instance OAI.Lech.SeparableOrder.orderFieldFaithful line 199
  21. lemma OAI.Lech.SeparableOrder.order_inherits_units line 204
  22. instance OAI.Lech.SeparableOrder.orderLocal line 219
  23. instance OAI.Lech.SeparableOrder.orderInclusionLocal line 224
  24. lemma OAI.Lech.SeparableOrder.uniform_power line 233
  25. instance OAI.Lech.SeparableOrder.orderFraction line 247
  26. lemma OAI.Lech.length_eq_of_semilinearEquiv line 278
  27. lemma OAI.Lech.length_span_eq_of_semilinearEquiv line 287
  28. lemma OAI.Lech.NormalizedLength.Tower.finiteLength_eq_iInf_shift line 303
  29. lemma OAI.Lech.NormalizedLength.Tower.length_eq_mul_of_stage_shift line 313
  30. lemma OAI.Lech.RootTower.rootMap_shift line 337
  31. def OAI.Lech.RootTower.rootShiftEquiv line 345
  32. lemma OAI.Lech.RootTower.rootShiftEquiv_val line 348
  33. def OAI.Lech.RootTower.restrictRootShift line 357
  34. lemma OAI.Lech.RootTower.regular_weight_shift line 381
  35. theorem OAI.Lech.RootTower.normalizedLength_root_equiv line 391
  36. lemma OAI.Lech.RootTower.map_inverse_frobenius line 417
  37. def OAI.Lech.RootTower.quotientRootEquiv line 425