OAI/Algebra/AuslanderReiten/Algebras/TrivialExtensionRadical.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArExplicit.TrivialExtension.projection line 10
  2. theorem OAI.ArExplicit.TrivialExtension.projection_apply line 18
  3. theorem OAI.ArExplicit.TrivialExtension.projection_surjective line 20
  4. theorem OAI.ArExplicit.TrivialExtension.mul_eq_zero_of_base_eq_zero line 23
  5. theorem OAI.ArExplicit.TrivialExtension.projection_kernel_square line 30
  6. theorem OAI.ArExplicit.TrivialExtension.radical_eq_comap line 38
  7. theorem OAI.ArExplicit.TrivialExtension.mem_jacobson_iff line 45
  8. def OAI.ArExplicit.T.diagonalAlg line 56
  9. theorem OAI.ArExplicit.T.diagonalAlg_surjective line 59
  10. theorem OAI.ArExplicit.T.radical_eq_ker_diagonal line 62
  11. def OAI.ArExplicit.T.semisimpleQuotientEquiv line 70
  12. theorem OAI.ArExplicit.T.jacobson_fourth_ne_bot line 75