OAI/Algebra/AuslanderReiten/Bar/ModuleBarNativeTransport.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArExplicit.ModuleBar.nativeEndpointBase line 16
  2. theorem OAI.ArExplicit.ModuleBar.nativeEndpointBase_smul line 32
  3. def OAI.ArExplicit.ModuleBar.nativeTransportBase line 36
  4. theorem OAI.ArExplicit.ModuleBar.nativeTransportBase_smul line 45
  5. theorem OAI.ArExplicit.ModuleBar.nativeTransportBase_d line 51
  6. def OAI.ArExplicit.ModuleBar.nativeEndpointEquiv line 61
  7. def OAI.ArExplicit.ModuleBar.nativeEndpointIso line 70
  8. def OAI.ArExplicit.ModuleBar.nativeTransportIso line 74
  9. theorem OAI.ArExplicit.ModuleBar.nativeTransport_augmentation line 79
  10. theorem OAI.ArExplicit.ModuleBar.nativeTransportBase_π line 88
  11. theorem OAI.ArExplicit.ModuleBar.nativeTransport_Hom line 93