OAI/Algebra/AuslanderReiten/BaseChange/ScalarExtensionHom.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArExplicit.scalarExtensionHomLinear line 18
  2. def OAI.ArExplicit.scalarExtensionHom line 32
  3. theorem OAI.ArExplicit.scalarExtensionHom_tmul line 37
  4. def OAI.ArExplicit.scalarExtensionHomCoordinates line 40
  5. theorem OAI.ArExplicit.scalarExtensionHom_bijective_pi line 46
  6. theorem OAI.ArExplicit.scalarExtensionHom_precomp line 79
  7. theorem OAI.ArExplicit.scalarExtensionHom_bijective line 88
  8. def OAI.ArExplicit.scalarExtensionHomEquiv line 113