OAI/Algebra/Determinantal/CoordinateFields.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PermanentBorder.CoordinateNormalization.exists_base_eval_ne_zero line 10
  2. def OAI.PermanentBorder.CoordinateNormalization.basisDeterminant line 22
  3. theorem OAI.PermanentBorder.CoordinateNormalization.eval_basisDeterminant line 26
  4. theorem OAI.PermanentBorder.CoordinateNormalization.exists_invertible_coordinate_gauge line 42
  5. def OAI.PermanentBorder.OrbitNormalization.intertwinerSpace line 77
  6. def OAI.PermanentBorder.OrbitNormalization.intertwinerEquivCentralizer line 91
  7. theorem OAI.PermanentBorder.OrbitNormalization.exists_normalized_intertwiner line 129
  8. def OAI.PermanentBorder.CentralizerParameters.coefficients line 162
  9. theorem OAI.PermanentBorder.CentralizerParameters.entry_expansion line 167
  10. theorem OAI.PermanentBorder.CentralizerParameters.eval_determinant line 176
  11. theorem OAI.PermanentBorder.CentralizerParameters.determinant_relation line 190
  12. theorem OAI.PermanentBorder.MatrixSubfield.mul_mem line 204
  13. theorem OAI.PermanentBorder.MatrixSubfield.unit_inv_mem line 210
  14. theorem OAI.PermanentBorder.ParameterBounds.field_adjoin_trdeg_lt_of_relation_fintype line 242
  15. theorem OAI.PermanentBorder.CommutingPairs.normalized_pair_field_bound line 263