OAI/RepresentationTheory/RestrictedTilting/PlaneMatrixTensor.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiberFunctorProof.matrixTensorLinear line 13
2. lemma OAI.FiberFunctorProof.matrixTensorLinear_apply line 18
3. lemma OAI.FiberFunctorProof.matrixTensorLinear_one line 23
4. lemma OAI.FiberFunctorProof.matrixTensorLinear_mul line 30
5. def OAI.FiberFunctorProof.matrixTensorRepresentation line 39
6. lemma OAI.FiberFunctorProof.matrixTensorRepresentation_apply line 49
7. lemma OAI.FiberFunctorProof.matrixTensor_rational line 62
8. lemma OAI.FiberFunctorProof.matrixTensor_planeCompatible line 84
9. lemma OAI.FiberFunctorProof.pi_regular_x line 95
10. lemma OAI.FiberFunctorProof.pi_regular_y line 103