OAI/Algebra/AuslanderReiten/Parameters.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ArExplicit.ParameterRing line 13
  2. abbrev OAI.ArExplicit.BaseField line 15
  3. def OAI.ArExplicit.parameter line 17
  4. abbrev OAI.ArExplicit.q line 20
  5. abbrev OAI.ArExplicit.H₁ line 21
  6. abbrev OAI.ArExplicit.H₂ line 22
  7. theorem OAI.ArExplicit.parameters_algebraicallyIndependent line 24
  8. theorem OAI.ArExplicit.parameter_ne_zero line 30
  9. theorem OAI.ArExplicit.parameter_pow_ne_one line 33
  10. theorem OAI.ArExplicit.parameter_pow_ne line 43
  11. theorem OAI.ArExplicit.q_pow_add_one_ne_zero line 53
  12. theorem OAI.ArExplicit.twist_eigenvalues_ne line 60
  13. theorem OAI.ArExplicit.twist_determinant_ne_zero line 67
  14. theorem OAI.ArExplicit.twist_determinant_ne_zero_after_extension line 76