OAI/NumberTheory/QuadraticForms/ScalarExtension.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

Tensor scalar extension and trace-form descent.

  1. def OAI.MultiplicityCounterexample.TensorAlgebraModule.rightAction line 16
  2. def OAI.MultiplicityCounterexample.TensorAlgebraModule.fullAction line 19
  3. lemma OAI.MultiplicityCounterexample.TensorAlgebraModule.smul_tmul_tmul line 27
  4. def OAI.MultiplicityCounterexample.CompletionFactorDescent.extendIsometry line 51
  5. lemma OAI.MultiplicityCounterexample.CompletionFactorDescent.extendIsometry_tmul line 66
  6. def OAI.MultiplicityCounterexample.CompletionFactorDescent.cancelIsometry line 77
  7. def OAI.MultiplicityCounterexample.CompletionFactorDescent.collapse line 110
  8. lemma OAI.MultiplicityCounterexample.CompletionFactorDescent.collapse_tmul line 123
  9. def OAI.MultiplicityCounterexample.CompletionFactorDescent.expand line 128
  10. lemma OAI.MultiplicityCounterexample.CompletionFactorDescent.expand_tmul line 132
  11. lemma OAI.MultiplicityCounterexample.CompletionFactorDescent.collapse_expand line 135
  12. lemma OAI.MultiplicityCounterexample.CompletionFactorDescent.expand_collapse line 140
  13. def OAI.MultiplicityCounterexample.CompletionFactorDescent.scalarAlgebraEquiv line 152
  14. lemma OAI.MultiplicityCounterexample.CompletionFactorDescent.scalarAlgebraEquiv_tmul line 157
  15. lemma OAI.MultiplicityCounterexample.CompletionFactorDescent.scalarAlgebraEquiv_symm_tmul line 161
  16. def OAI.MultiplicityCounterexample.CompletionFactorDescent.scalarAlgebraForm line 166
  17. lemma OAI.MultiplicityCounterexample.CompletionFactorDescent.scalarAlgebraForm_tmul line 170
  18. def OAI.MultiplicityCounterexample.CompletionFactorDescent.scalarAlgebraIsometry line 178
  19. lemma OAI.MultiplicityCounterexample.CompletionFactorDescent.scalarAlgebraForm_restrict line 186
  20. def OAI.MultiplicityCounterexample.CompletionFactorDescent.descendIsometry line 199
  21. def OAI.MultiplicityCounterexample.CompletionFactorDescent.factorMap line 220
  22. lemma OAI.MultiplicityCounterexample.CompletionFactorDescent.factorMap_tmul line 224
  23. def OAI.MultiplicityCounterexample.CompletionFactorDescent.descendAlongPlace line 227
  24. def OAI.MultiplicityCounterexample.TraceBaseChange.perfectBase line 248
  25. lemma OAI.MultiplicityCounterexample.TraceBaseChange.dualBase_tmul line 253
  26. lemma OAI.MultiplicityCounterexample.TraceBaseChange.perfectBase_apply line 262
  27. lemma OAI.MultiplicityCounterexample.TraceBaseChange.baseChange_nondegenerate line 276
  28. lemma OAI.MultiplicityCounterexample.TraceBaseChange.trace_one_tmul line 293
  29. lemma OAI.MultiplicityCounterexample.TraceBaseChange.trace_tmul line 299
  30. lemma OAI.MultiplicityCounterexample.TraceBaseChange.traceForm_baseChange line 305
  31. lemma OAI.MultiplicityCounterexample.TraceBaseChange.traceForm_nondegenerate_baseChange line 322
  32. def OAI.MultiplicityCounterexample.TraceBaseChange.traceDual line 327
  33. lemma OAI.MultiplicityCounterexample.TraceBaseChange.traceDual_apply line 330
  34. lemma OAI.MultiplicityCounterexample.TraceBaseChange.trace_pairing_ext line 334
  35. def OAI.MultiplicityCounterexample.TraceBaseChange.traceFunctional line 347
  36. def OAI.MultiplicityCounterexample.TraceBaseChange.lift line 353
  37. lemma OAI.MultiplicityCounterexample.TraceBaseChange.trace_lift line 356
  38. lemma OAI.MultiplicityCounterexample.TraceBaseChange.trace_lift_one line 361
  39. lemma OAI.MultiplicityCounterexample.TraceBaseChange.lift_add_left line 365
  40. lemma OAI.MultiplicityCounterexample.TraceBaseChange.lift_add_right line 371
  41. lemma OAI.MultiplicityCounterexample.TraceBaseChange.lift_smul_left line 377
  42. theorem OAI.MultiplicityCounterexample.TraceBaseChange.preserves_iff line 383
  43. lemma OAI.MultiplicityCounterexample.TraceBaseChange.lift_unique line 395
  44. lemma OAI.MultiplicityCounterexample.TensorEquivariant.rightAction_algebraMap line 416
  45. def OAI.MultiplicityCounterexample.TensorEquivariant.intertwiningScalars line 421
  46. lemma OAI.MultiplicityCounterexample.TensorEquivariant.intertwines_all line 438
  47. lemma OAI.MultiplicityCounterexample.TensorEquivariant.map_smul_tensor line 450
  48. def OAI.MultiplicityCounterexample.TensorEquivariant.linearOverTensor line 460
  49. def OAI.MultiplicityCounterexample.TensorEquivariant.equivOverTensor line 467
  50. def OAI.MultiplicityCounterexample.CompletionTraceDescent.traceForm line 490
  51. lemma OAI.MultiplicityCounterexample.CompletionTraceDescent.traceForm_apply line 499
  52. lemma OAI.MultiplicityCounterexample.CompletionTraceDescent.trace_scalarAlgebraForm line 503
  53. def OAI.MultiplicityCounterexample.CompletionTraceDescent.scalarIsometryOfTrace line 516
  54. def OAI.MultiplicityCounterexample.CompletionTraceDescent.descendTraceAtPlace line 538