OAI/NumberTheory/QuadraticForms/CyclotomicComponents.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

Cyclotomic operator components and nondegenerate forms.

  1. lemma OAI.MultiplicityCounterexample.PolynomialComponentRestriction.range_baseChange line 17
  2. def OAI.MultiplicityCounterexample.PolynomialComponentRestriction.rangeBaseChangeEquiv line 24
  3. lemma OAI.MultiplicityCounterexample.PolynomialComponentRestriction.rangeBaseChangeEquiv_coe line 29
  4. lemma OAI.MultiplicityCounterexample.PolynomialComponentRestriction.map_ranges line 33
  5. def OAI.MultiplicityCounterexample.PolynomialComponentRestriction.restrictRangeEquiv line 46
  6. lemma OAI.MultiplicityCounterexample.PolynomialComponentRestriction.restrictRangeEquiv_subtype line 53
  7. lemma OAI.MultiplicityCounterexample.PolynomialComponentRestriction.restrictForm_baseChange line 66
  8. theorem OAI.MultiplicityCounterexample.PolynomialComponentRestriction.restrictRangeEquiv_preserves line 77
  9. lemma OAI.MultiplicityCounterexample.CyclicComponent.commute_eval line 97
  10. abbrev OAI.MultiplicityCounterexample.CyclicComponent.component line 99
  11. def OAI.MultiplicityCounterexample.CyclicComponent.componentOperator line 100
  12. lemma OAI.MultiplicityCounterexample.CyclicComponent.componentOperator_coe line 106
  13. lemma OAI.MultiplicityCounterexample.PolynomialComponentRestriction.intertwines_pow line 118
  14. lemma OAI.MultiplicityCounterexample.PolynomialComponentRestriction.intertwines_aeval line 128
  15. def OAI.MultiplicityCounterexample.PolynomialComponentRestriction.restrictComponentEquiv line 141
  16. lemma OAI.MultiplicityCounterexample.PolynomialComponentRestriction.componentOperator_baseChange_coe line 147
  17. theorem OAI.MultiplicityCounterexample.PolynomialComponentRestriction.restrictComponentEquiv_intertwines line 155
  18. theorem OAI.MultiplicityCounterexample.PolynomialComponentRestriction.component_local_datum line 171
  19. def OAI.MultiplicityCounterexample.CyclicComponent.action line 192
  20. abbrev OAI.MultiplicityCounterexample.CyclicComponent.scalarModule line 203
  21. instance OAI.MultiplicityCounterexample.CyclicComponent.scalarTower line 206
  22. lemma OAI.MultiplicityCounterexample.CyclicComponent.root_smul line 216
  23. lemma OAI.MultiplicityCounterexample.CyclicComponent.eval_componentOperator line 222
  24. lemma OAI.MultiplicityCounterexample.CyclicComponent.component_annihilated line 237
  25. def OAI.MultiplicityCounterexample.CyclicComponent.componentScalarModule line 246
  26. lemma OAI.MultiplicityCounterexample.ComponentRootLocalComparison.rightAction_root line 261
  27. theorem OAI.MultiplicityCounterexample.ComponentRootLocalComparison.component_root_local_datum line 274
  28. def OAI.MultiplicityCounterexample.RealCyclotomicField.realGeneratorField line 297
  29. lemma OAI.MultiplicityCounterexample.RealCyclotomicField.realGeneratorField_le_maximalReal line 300
  30. lemma OAI.MultiplicityCounterexample.RealCyclotomicField.realGeneratorField_finrank_le_two line 313
  31. theorem OAI.MultiplicityCounterexample.RealCyclotomicField.realGeneratorField_eq_maximalReal line 340
  32. instance OAI.MultiplicityCounterexample.CyclotomicQuotient.cycloIrred line 368
  33. abbrev OAI.MultiplicityCounterexample.CyclotomicQuotient.E line 371
  34. instance OAI.MultiplicityCounterexample.CyclotomicQuotient.finite line 373
  35. instance OAI.MultiplicityCounterexample.CyclotomicQuotient.numberField line 376
  36. lemma OAI.MultiplicityCounterexample.CyclotomicQuotient.root_primitive line 378
  37. instance OAI.MultiplicityCounterexample.CyclotomicQuotient.cyclotomic line 383
  38. lemma OAI.MultiplicityCounterexample.CyclotomicQuotient.cm line 399
  39. instance OAI.MultiplicityCounterexample.SourceCyclotomicField.quotientCM line 410
  40. def OAI.MultiplicityCounterexample.SourceCyclotomicField.F line 412
  41. lemma OAI.MultiplicityCounterexample.SourceCyclotomicField.conj_root line 415
  42. lemma OAI.MultiplicityCounterexample.SourceCyclotomicField.root_nonreal line 425
  43. theorem OAI.MultiplicityCounterexample.SourceCyclotomicField.F_eq_maximalReal line 440
  44. instance OAI.MultiplicityCounterexample.SourceCyclotomicField.F_totallyReal line 444
  45. lemma OAI.MultiplicityCounterexample.SourceCyclotomicField.conj_fixed line 447
  46. lemma OAI.MultiplicityCounterexample.SourceCyclotomicField.exists_scalar_of_conj_fixed line 452
  47. lemma OAI.MultiplicityCounterexample.SourceCyclotomicField.F_finrank line 458
  48. lemma OAI.MultiplicityCounterexample.ComponentNondegenerate.inverse_adjoint line 487
  49. lemma OAI.MultiplicityCounterexample.ComponentNondegenerate.power_adjoint line 495
  50. lemma OAI.MultiplicityCounterexample.ComponentNondegenerate.polynomial_adjoint line 504
  51. lemma OAI.MultiplicityCounterexample.ComponentNondegenerate.orthogonal_range line 518
  52. lemma OAI.MultiplicityCounterexample.ComponentNondegenerate.ranges_span line 524
  53. theorem OAI.MultiplicityCounterexample.ComponentNondegenerate.restriction_nondegenerate line 541
  54. def OAI.MultiplicityCounterexample.TraceHermitian.adjointScalars line 572
  55. theorem OAI.MultiplicityCounterexample.TraceHermitian.adjointRule_of_generator line 588