OAI/NumberTheory/QuadraticForms/ComponentLengths.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Component length forms at finite and infinite places.

  1. def OAI.MultiplicityCounterexample.SourceComponentLengthAtPlaces.conjugation line 21
  2. lemma OAI.MultiplicityCounterexample.SourceComponentLengthAtPlaces.component_adjoint line 25
  3. lemma OAI.MultiplicityCounterexample.SourceComponentLengthAtPlaces.component_selfAdjoint line 44
  4. def OAI.MultiplicityCounterexample.SourceComponentLengthAtPlaces.componentLength line 53
  5. lemma OAI.MultiplicityCounterexample.SourceComponentLengthAtPlaces.componentLength_value line 61
  6. lemma OAI.MultiplicityCounterexample.SourceComponentLengthAtPlaces.inverse_root line 75
  7. lemma OAI.MultiplicityCounterexample.SourceComponentLengthAtPlaces.componentLength_nondegenerate line 80
  8. def OAI.MultiplicityCounterexample.SourceComponentLengthAtPlaces.RationalPlaceDatum line 96
  9. lemma OAI.MultiplicityCounterexample.SourceComponentLengthAtPlaces.componentDatum line 103
  10. theorem OAI.MultiplicityCounterexample.SourceComponentLengthAtPlaces.componentLength_isometric_at_all_places line 117
  11. lemma OAI.MultiplicityCounterexample.CyclotomicComponentFactor.cyclotomic_dvd line 151
  12. theorem OAI.MultiplicityCounterexample.CyclotomicComponentFactor.exists_complement line 157
  13. lemma OAI.MultiplicityCounterexample.CyclotomicComponentFactor.commute_aeval line 168
  14. theorem OAI.MultiplicityCounterexample.CyclotomicComponentFactor.range_eq_ker line 171
  15. lemma OAI.MultiplicityCounterexample.CyclotomicComponentFactor.component_annihilation line 190
  16. theorem OAI.MultiplicityCounterexample.CyclotomicComponentFactor.semisimple line 197
  17. def OAI.MultiplicityCounterexample.HasseMinkowskiGap.AllPlacesIsometric line 212
  18. def OAI.MultiplicityCounterexample.HasseMinkowskiGap.NumberFieldQuadraticLocalGlobal line 219
  19. theorem OAI.MultiplicityCounterexample.SourceComponentLengthAtPlaces.finite_order_component_hasse_input line 239
  20. lemma OAI.MultiplicityCounterexample.IdentityComponentAtPlaces.identity_on_component line 279
  21. lemma OAI.MultiplicityCounterexample.IdentityComponentAtPlaces.restriction_nondegenerate line 288
  22. lemma OAI.MultiplicityCounterexample.IdentityComponentAtPlaces.rat_selfAdjoint line 297
  23. lemma OAI.MultiplicityCounterexample.IdentityComponentAtPlaces.fixedForm_rat line 301
  24. lemma OAI.MultiplicityCounterexample.IdentityComponentAtPlaces.fixedForm_rat_canonical line 306
  25. lemma OAI.MultiplicityCounterexample.IdentityComponentAtPlaces.componentDatum line 311
  26. lemma OAI.MultiplicityCounterexample.IdentityComponentAtPlaces.restricted_forms_at_every_finitePlace line 319
  27. lemma OAI.MultiplicityCounterexample.IdentityComponentAtPlaces.restricted_forms_at_every_infinitePlace line 337
  28. lemma OAI.MultiplicityCounterexample.IdentityComponentAtPlaces.diagonal_nondegenerate line 353
  29. lemma OAI.MultiplicityCounterexample.IdentityComponentAtPlaces.diagonal_baseChange line 359
  30. def OAI.MultiplicityCounterexample.IdentityComponentAtPlaces.diagonalIsometryAtPlace line 366
  31. theorem OAI.MultiplicityCounterexample.IdentityComponentAtPlaces.component_all_places line 375
  32. theorem OAI.MultiplicityCounterexample.IdentityComponentAtPlaces.finite_order_identity_hasse_input line 391