OAI/Algebra/AuslanderReiten/BaseChange/ScalarExtensionCokernel.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.ArExplicit.scalarExtensionCokernelEquivline 17 - def
OAI.ArExplicit.scalarExtensionEquivline 24 - theorem
OAI.ArExplicit.scalarExtension_regular_smulline 31 - theorem
OAI.ArExplicit.scalarExtensionModule_eq_regularline 42