OAI/NumberTheory/Ostmann/Supply/CRTPrimitiveEnergy.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Supply.crtUnitsEquiv line 18
  2. theorem OAI.Ostmann.Supply.crtUnitsEquiv_apply line 23
  3. theorem OAI.Ostmann.Supply.addChar_sum_eq_prod line 32
  4. def OAI.Ostmann.Supply.coordinateChar line 41
  5. theorem OAI.Ostmann.Supply.coordinateChar_apply line 48
  6. theorem OAI.Ostmann.Supply.coordinateChar_isPrimitive line 52
  7. theorem OAI.Ostmann.Supply.addChar_pi_eq_prod line 62
  8. theorem OAI.Ostmann.Supply.primitive_sum_units_field line 70
  9. theorem OAI.Ostmann.Supply.primitive_sum_units_pi line 91
  10. theorem OAI.Ostmann.Supply.stdAddChar_sum_units_equiv line 111
  11. theorem OAI.Ostmann.Supply.stdAddChar_sum_units_prod line 135
  12. theorem OAI.Ostmann.Supply.stdAddChar_sum_units_squarefree line 146
  13. def OAI.Ostmann.Supply.normalizedCharSum line 165
  14. theorem OAI.Ostmann.Supply.norm_stdAddChar_sum_sq line 168
  15. theorem OAI.Ostmann.Supply.norm_normalizedCharSum_sq line 185
  16. theorem OAI.Ostmann.Supply.normalizedCharSum_primitive_energy_complex line 192
  17. theorem OAI.Ostmann.Supply.normalizedCharSum_primitive_energy line 217
  18. theorem OAI.Ostmann.Supply.stdAddChar_mul_nat_eq_exp line 229
  19. theorem OAI.Ostmann.Supply.normalizedExpSum_eq_normalizedCharSum line 239
  20. theorem OAI.Ostmann.Supply.normalizedExpSum_primitive_energy line 249
  21. theorem OAI.Ostmann.Supply.normalizedExpSum_primitive_energy_complex line 259