OAI/Algebra/AuslanderReiten/Evaluation/ConcreteFreeCoefficient.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ArExplicit.T.threeValue line 9
2. theorem OAI.ArExplicit.T.identityValue line 15
3. theorem OAI.ArExplicit.T.comp_hom_apply line 19
4. theorem OAI.ArExplicit.T.transferFunctionValue line 22
5. theorem OAI.ArExplicit.T.coefficientTensorValue line 38
6. theorem OAI.ArExplicit.T.freeTransferValue line 50
7. theorem OAI.ArExplicit.T.rawCoordinateValue line 56
8. theorem OAI.ArExplicit.T.rawCoordinateDirect line 61
9. theorem OAI.ArExplicit.T.transferRawValues line 68

   Source comment

   Specialize the equality of coordinate functions after computing the tensor value.

   private theorem transferRawValues :
       type_of% (@transferFunctionValue _ _ _ _ (rawCoordinateDirect q hq)) :=
   …

   Mentions: OAI.ArExplicit.T.transferFunctionValue, OAI.ArExplicit.T.rawCoordinateDirect, OAI.ArExplicit.q

10. theorem OAI.ArExplicit.T.freeCoordinateRaw_tmul_transfer line 72