OAI/LinearAlgebra/MatrixFields/Construction/InitialHistories.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.shapeCounts_fiber line 17
2. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.shapeCountFiberEquiv line 24
3. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.InitialPlacement line 31
4. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.InitialShapeFiber line 33
5. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.initialClassPositionEquiv line 36
6. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.initialClassPosition_shape line 43
7. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.initialStateEquiv line 50