OAI/Combinatorics/Progressions/Linear/AntisymmetricPairProjections.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.NativeMultidegreeNilcharacter.pairComponentPolynomial line 24
2. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.pairComponentPolynomial_out_eq line 28
3. theorem OAI.Erdos3.NativeSampleCorrelation.antisymmetricPairProjection_layers line 41
4. def OAI.Erdos3.NativeSampleCorrelation.antisymmetricPairPolynomialMap line 46
5. theorem OAI.Erdos3.NativeSampleCorrelation.antisymmetricPairPolynomialMap_log line 53
6. theorem OAI.Erdos3.NativeSampleCorrelation.antisymmetricPairPolynomialMap_eq line 60
7. theorem OAI.Erdos3.NativeSampleCorrelation.antisymmetricPairPolynomialMap_constant line 71
8. theorem OAI.Erdos3.NativeSampleCorrelation.antisymmetricPairProjection_lattice line 81
9. def OAI.Erdos3.NativeSampleCorrelation.antisymmetricPairCoordinateIndex line 87
10. theorem OAI.Erdos3.NativeSampleCorrelation.antisymmetricPairProjection_repr line 91