OAI/NumberTheory/QuadraticForms/LocalTrace.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

Local trace and cyclotomic length comparisons.

  1. def OAI.MultiplicityCounterexample.CompletionPlaceMaps.rationalAbs line 18
  2. lemma OAI.MultiplicityCounterexample.CompletionPlaceMaps.rationalAbs_apply line 25
  3. def OAI.MultiplicityCounterexample.CompletionPlaceMaps.fromWithVal line 29
  4. lemma OAI.MultiplicityCounterexample.CompletionPlaceMaps.continuous_fromWithVal line 32
  5. def OAI.MultiplicityCounterexample.CompletionPlaceMaps.padicMap line 54
  6. theorem OAI.MultiplicityCounterexample.CompletionPlaceMaps.exists_padicMap line 59
  7. instance OAI.MultiplicityCounterexample.CompletionPlaceMaps.finitePlaceCharZero line 76
  8. lemma OAI.MultiplicityCounterexample.CompletionPlaceMaps.rationalAbs_finitePlace_nontrivial line 79
  9. lemma OAI.MultiplicityCounterexample.CompletionPlaceMaps.rationalAbs_finitePlace_bounded line 89
  10. theorem OAI.MultiplicityCounterexample.CompletionPlaceMaps.exists_finitePlace_padicAlgHom line 96
  11. instance OAI.MultiplicityCounterexample.CompletionPlaceMaps.infinitePlaceCharZero line 107
  12. def OAI.MultiplicityCounterexample.CompletionPlaceMaps.infinitePlaceRealAlgHom line 110
  13. def OAI.MultiplicityCounterexample.NumberFieldTraceLocalComparison.LocalTraceIsometry line 132
  14. theorem OAI.MultiplicityCounterexample.NumberFieldTraceLocalComparison.isometric_at_every_finitePlace line 140
  15. theorem OAI.MultiplicityCounterexample.NumberFieldTraceLocalComparison.isometric_at_every_infinitePlace line 154
  16. lemma OAI.MultiplicityCounterexample.TraceHermitian.trace_pairing_ext line 178
  17. def OAI.MultiplicityCounterexample.TraceHermitian.traceFunctional line 184
  18. def OAI.MultiplicityCounterexample.TraceHermitian.lift line 189
  19. lemma OAI.MultiplicityCounterexample.TraceHermitian.trace_lift line 193
  20. lemma OAI.MultiplicityCounterexample.TraceHermitian.trace_lift_one line 200
  21. lemma OAI.MultiplicityCounterexample.TraceHermitian.lift_add_left line 204
  22. lemma OAI.MultiplicityCounterexample.TraceHermitian.lift_add_right line 210
  23. lemma OAI.MultiplicityCounterexample.TraceHermitian.lift_smul_left line 216
  24. def OAI.MultiplicityCounterexample.TraceHermitian.AdjointRule line 224
  25. lemma OAI.MultiplicityCounterexample.TraceHermitian.lift_smul_right line 228
  26. lemma OAI.MultiplicityCounterexample.TraceHermitian.trace_sigma line 235
  27. lemma OAI.MultiplicityCounterexample.TraceHermitian.lift_symmetric line 239
  28. lemma OAI.MultiplicityCounterexample.TraceHermitian.lift_nondegenerate_left line 246
  29. lemma OAI.MultiplicityCounterexample.TraceHermitian.lift_nondegenerate_right line 252
  30. theorem OAI.MultiplicityCounterexample.TraceHermitian.preserves_iff line 258
  31. theorem OAI.MultiplicityCounterexample.TraceHermitian.lift_unique line 269
  32. def OAI.MultiplicityCounterexample.FixedFieldLocalComparison.SelfAdjointScalars line 290
  33. def OAI.MultiplicityCounterexample.FixedFieldLocalComparison.fixedForm line 293
  34. lemma OAI.MultiplicityCounterexample.FixedFieldLocalComparison.fixedForm_apply line 306
  35. lemma OAI.MultiplicityCounterexample.FixedFieldLocalComparison.trace_fixedForm line 309
  36. lemma OAI.MultiplicityCounterexample.FixedFieldLocalComparison.fixedForm_symmetric line 314
  37. lemma OAI.MultiplicityCounterexample.FixedFieldLocalComparison.fixedForm_nondegenerate line 321
  38. theorem OAI.MultiplicityCounterexample.FixedFieldLocalComparison.localTraceIsometry_of_equivariant line 341
  39. lemma OAI.MultiplicityCounterexample.FixedFieldBridge.rightAction_tower line 369
  40. lemma OAI.MultiplicityCounterexample.FixedFieldBridge.intertwines_fixedScalars line 378
  41. lemma OAI.MultiplicityCounterexample.FixedFieldPrimitive.exists_primitive line 393
  42. lemma OAI.MultiplicityCounterexample.CyclotomicPlaceComparison.selfAdjointScalars_of_fixed_involution line 415
  43. def OAI.MultiplicityCounterexample.CyclotomicPlaceComparison.LocalEquivariantIsometry line 423
  44. lemma OAI.MultiplicityCounterexample.CyclotomicPlaceComparison.localTraceIsometry_of_cyclotomic line 429
  45. theorem OAI.MultiplicityCounterexample.CyclotomicPlaceComparison.fixedForm_isometric_at_every_finitePlace line 440
  46. theorem OAI.MultiplicityCounterexample.CyclotomicPlaceComparison.fixedForm_isometric_at_every_infinitePlace line 452
  47. theorem OAI.MultiplicityCounterexample.TraceTowerCompatibility.lift_fixed_eq_trace_lift line 477
  48. theorem OAI.MultiplicityCounterexample.TraceTowerCompatibility.lift_fixed_diagonal line 493
  49. def OAI.MultiplicityCounterexample.LengthBaseChange.halfForm line 510
  50. def OAI.MultiplicityCounterexample.LengthBaseChange.lengthForm line 512
  51. lemma OAI.MultiplicityCounterexample.LengthBaseChange.halfForm_apply line 515
  52. lemma OAI.MultiplicityCounterexample.LengthBaseChange.lengthForm_apply line 519
  53. lemma OAI.MultiplicityCounterexample.LengthBaseChange.halfForm_symmetric line 523
  54. lemma OAI.MultiplicityCounterexample.LengthBaseChange.halfForm_nondegenerate line 526
  55. lemma OAI.MultiplicityCounterexample.LengthBaseChange.lengthForm_nondegenerate line 540
  56. lemma OAI.MultiplicityCounterexample.LengthBaseChange.lengthForm_baseChange line 550
  57. def OAI.MultiplicityCounterexample.LengthBaseChange.lengthIsometryAtPlace line 558
  58. def OAI.MultiplicityCounterexample.CyclotomicLengthLocalComparison.sourceLength line 584
  59. theorem OAI.MultiplicityCounterexample.CyclotomicLengthLocalComparison.sourceLength_value line 587
  60. theorem OAI.MultiplicityCounterexample.CyclotomicLengthLocalComparison.sourceLength_nondegenerate line 600
  61. theorem OAI.MultiplicityCounterexample.CyclotomicLengthLocalComparison.length_isometric_at_every_finitePlace line 606
  62. theorem OAI.MultiplicityCounterexample.CyclotomicLengthLocalComparison.length_isometric_at_every_infinitePlace line 618