OAI/Algebra/Finitistic/Ordinary/OrdinaryBalancedCongruence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.BalancedTensor.congr line 14

   Source documentation

   Actual balanced tensor congruence under module equivalences in both factors.

   def congr (e : M ≃ₗ[Aᵐᵒᵖ] M') (f : N ≃ₗ[A] N') : Tensor k A M N ≃ₗ[k] Tensor k A M' N' where
   …

   Mentions: OAI.LittleFinitistic.BalancedTensor.Tensor