OAI/Algebra/Finitistic/Dimension/PDResidueAssociativity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LittleFinitistic.PDResidueAssociativity.coefficient line 18
  2. def OAI.LittleFinitistic.PDResidueAssociativity.inner line 32
  3. theorem OAI.LittleFinitistic.PDResidueAssociativity.inner_mk line 41
  4. def OAI.LittleFinitistic.PDResidueAssociativity.pair line 45
  5. def OAI.LittleFinitistic.PDResidueAssociativity.forward line 64
  6. def OAI.LittleFinitistic.PDResidueAssociativity.unit line 78
  7. def OAI.LittleFinitistic.PDResidueAssociativity.inverse line 81
  8. theorem OAI.LittleFinitistic.PDResidueAssociativity.inverse_mk line 95
  9. def OAI.LittleFinitistic.PDResidueAssociativity.equiv line 100

    Source documentation

    Actual balanced associativity S tensor_D (D tensor_A V) = S tensor_A V, with the right A action restricted along f.

    def equiv : BalancedTensor.Tensor k D S DV ≃ₗ[k] T :=
…

    Mentions: OAI.LittleFinitistic.BalancedTensor.Tensor