OAI/Algebra/Finitistic/Ordinary/OrdinaryLeftTensorCongruence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.LeftTensor.congr line 17

   Source documentation

   Actual balanced tensor congruence retaining the outside left action.

   def congr (f : M ≃ₗ[Aᵐᵒᵖ] M') (hf : ∀ (s : S) m, f (s • m) = s • f m)
       (g : N ≃ₗ[A] N') : LeftTensor k A S M N ≃ₗ[S] LeftTensor k A S M' N' where
   …

   Mentions: OAI.LittleFinitistic.LeftTensor