OAI/NumberTheory/PiExponent/Approximation/FormalMatrixBridge.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.FormalMatrixBridge.flatten line 14
2. theorem OAI.PiExponent.FormalMatrixBridge.coeff_flatten line 20
3. theorem OAI.PiExponent.FormalMatrixBridge.flatten_C line 28
4. theorem OAI.PiExponent.FormalMatrixBridge.flatten_X line 36
5. theorem OAI.PiExponent.FormalMatrixBridge.flatten_literalJetSubstitution line 54
6. theorem OAI.PiExponent.FormalMatrixBridge.coeff_truncatedFormalJet line 72
7. theorem OAI.PiExponent.FormalMatrixBridge.exponentVector_tail line 81
8. theorem OAI.PiExponent.FormalMatrixBridge.entry_eq_coeff_truncatedFormalJet line 87
9. theorem OAI.PiExponent.FormalMatrixBridge.truncatedLogMatrix_mulVec_eq_coeff line 98