OAI/LinearAlgebra/MatrixFields/Parameters/ParametersCompatibility.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.statisticLaw line 12
2. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.statisticComplement line 17
3. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.statisticLaw_complement line 19
4. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.statisticLaw_outside_support line 23
5. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.littleLaw_eq_statisticLaw line 28
6. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.littleLaw_outside_support line 31
7. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.littleLaw_complement line 35
8. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.child_statistic_weight_bounded line 46
9. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldParameters.pair_complement_involution line 49