OAI/LinearAlgebra/MatrixFields/Histories/InitialOrbit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialOrbit.source_total line 15
2. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialOrbit.decodeShape_injective line 22
3. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialOrbit.decodeShape_mem_shapes line 30
4. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialOrbit.initialShapeCode_eq_iff line 42
5. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialOrbit.weighted_shape_fiber_count line 52
6. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldInitialOrbit.weighted_fiber_count line 58