OAI/Algebra/Finitistic/Ordinary/OrdinarySignedExactness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LittleFinitistic.exact_units_smul line 13

   Source documentation

   Multiplying both differentials by an integer unit preserves exactness.

   theorem exact_units_smul (u : ℤˣ) (f : E →ₗ[R] F) (g : F →ₗ[R] G)
       (h : Function.Exact f g) : Function.Exact (u • f) (u • g) := by
   …