OAI/GroupTheory/PeriodicGroups/Steinberg/MatrixUnits.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SourceBurnside.Kernel.numericUnits line 12
  2. lemma OAI.SourceBurnside.Kernel.bigBasisUnits_entry line 14
  3. lemma OAI.SourceBurnside.Kernel.bigBasisUnits_map line 21
  4. lemma OAI.SourceBurnside.Kernel.numerical_big_lift line 33
  5. lemma OAI.SourceBurnside.Kernel.numeric_conj_scalar line 43
  6. lemma OAI.SourceBurnside.Kernel.numeric_conj_matrix line 49
  7. lemma OAI.SourceBurnside.Kernel.matrixEval_conjugacy line 55
  8. theorem OAI.SourceBurnside.Kernel.stable_numerical_similarity line 70
  9. def OAI.SourceBurnside.Kernel.pascalMatrix line 88
  10. lemma OAI.SourceBurnside.Kernel.pascal_lower line 89
  11. lemma OAI.SourceBurnside.Kernel.pascal_det line 94
  12. lemma OAI.SourceBurnside.Kernel.matrix_mul_truncated line 97
  13. lemma OAI.SourceBurnside.Kernel.cyclic_mul_matrix line 120
  14. lemma OAI.SourceBurnside.Kernel.pascal_times_unipotent line 131
  15. lemma OAI.SourceBurnside.Kernel.power_two_choose line 141
  16. lemma OAI.SourceBurnside.Kernel.cyclic_pascal line 150
  17. theorem OAI.SourceBurnside.Kernel.cyclic_triangularization line 162
  18. lemma OAI.SourceBurnside.Kernel.one_add_truncated_upper line 180
  19. lemma OAI.SourceBurnside.Kernel.one_add_truncated_diag line 185
  20. theorem OAI.SourceBurnside.Kernel.stable_cyclic_evaluation line 189
  21. theorem OAI.SourceBurnside.Kernel.stable_diagonal_evaluations line 200
  22. def OAI.SourceBurnside.Kernel.copyMatrixHom line 214
  23. def OAI.SourceBurnside.Kernel.copyUnitsHom line 217
  24. lemma OAI.SourceBurnside.Kernel.copyUnitsHom_e line 219
  25. lemma OAI.SourceBurnside.Kernel.copy_representation line 233
  26. lemma OAI.SourceBurnside.Kernel.copy_kernel line 238
  27. def OAI.SourceBurnside.Kernel.swapUnits line 243
  28. lemma OAI.SourceBurnside.Kernel.swap_coefficient_single line 248
  29. theorem OAI.SourceBurnside.Kernel.stable_copy_eq line 265
  30. lemma OAI.SourceBurnside.Kernel.pad_ringMap line 287
  31. lemma OAI.SourceBurnside.Kernel.copy_ringMap line 294
  32. lemma OAI.SourceBurnside.Kernel.diagonalCopy_ringMap line 301
  33. lemma OAI.SourceBurnside.Kernel.stable_diagonalCopy_pow line 310
  34. lemma OAI.SourceBurnside.Kernel.stable_ground_diagonal_periodic line 320
  35. theorem OAI.SourceBurnside.Kernel.stable_word_copy_torsion line 329
  36. theorem OAI.SourceBurnside.Kernel.polynomial_kernel_copy_torsion line 352
  37. lemma OAI.SourceBurnside.WordAlgebra.Table.scalarEval_zero line 381
  38. lemma OAI.SourceBurnside.WordAlgebra.Table.scalarEval_one line 387
  39. theorem OAI.SourceBurnside.ConcreteSource.kernel_coordinate_torsion line 398
  40. def OAI.SourceBurnside.Kernel.permutationUnits line 421
  41. lemma OAI.SourceBurnside.Kernel.numerical_lift line 426
  42. lemma OAI.SourceBurnside.Kernel.permutation_conjugates_e line 433
  43. theorem OAI.SourceBurnside.Kernel.stable_permutation_fixed line 446
  44. lemma OAI.SourceBurnside.Kernel.coordinateMap_comp line 466
  45. theorem OAI.SourceBurnside.Kernel.stable_copy_to_standard line 474
  46. lemma OAI.SourceBurnside.Kernel.pad_standard line 501
  47. theorem OAI.SourceBurnside.Kernel.polynomial_kernel_standard_torsion line 511
  48. theorem OAI.SourceBurnside.ConcreteSource.kernel_standard_stable_torsion line 529