OAI/Algebra/AuslanderReiten/Triangular/ConvertedScalarExtension.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.ConvertedAlgebra.diagonalAlg line 17
2. theorem OAI.ArExplicit.ConvertedAlgebra.diagonalAlg_surjective line 20
3. theorem OAI.ArExplicit.ConvertedAlgebra.radical_eq_ker_diagonal line 24
4. def OAI.ArExplicit.ConvertedAlgebra.scalarExtensionQuotientEquiv line 34
5. theorem OAI.ArExplicit.ConvertedAlgebra.scalarExtension_jacobson_fourth_ne_bot line 40