OAI/Algebra/AuslanderReiten/Algebras/Radical.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ArExplicit.nilIdeal_le_jacobson line 11
  2. theorem OAI.ArExplicit.nilpotentIdeal_le_jacobson line 25
  3. theorem OAI.ArExplicit.jacobson_eq_kernel line 34
  4. theorem OAI.ArExplicit.jacobson_eq_comap_of_nil_kernel line 44
  5. theorem OAI.ArExplicit.mem_jacobson_prod_iff line 51
  6. theorem OAI.ArExplicit.jacobson_prod_eq_bot line 67
  7. theorem OAI.ArExplicit.jacobson_eq_bot_of_equiv line 76
  8. theorem OAI.ArExplicit.field_jacobson_eq_bot line 85
  9. theorem OAI.ArExplicit.field_pi_jacobson_eq_bot line 89
  10. theorem OAI.ArExplicit.map_mem_ideal_pow line 99
  11. theorem OAI.ArExplicit.radical_pow_ne_bot_of_injective line 109