OAI/Combinatorics/Progressions/Geometry/AllocatedExternalCandidateSpatialNativeAutomaticLongGeometry.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.NilpotentLieFiltration.piRealOrbit_polynomialOrbitRealChart_log line 20
2. theorem OAI.Erdos3.NilpotentLieFiltration.piRealOrbit_polynomialOrbitRealChart line 38
3. theorem OAI.Erdos3.NilpotentLieFiltration.piRealOrbit_polynomialOrbitRealChart_coordinates line 49
4. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.CommonFactors line 113
5. theorem OAI.Erdos3.VectorPolynomial.compose_exponential_mass_losses line 148

   Also declared: OAI/Combinatorics/Progressions/Geometry/AllocatedExternalCandidateSpatialNativeLongCommonFactors.lean:96 (same declaration text).

6. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedExternalCandidateSpatialNativeFamily_common_factors line 158
7. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.actualSourceProblemOn line 306
8. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.actualJointProblemOn line 324
9. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.actualJointProblemOn_productive line 331
10. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.actualJointProblemOn_keep line 337
11. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.actualJointProblemOn_orbit line 343
12. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.CommonFactors.exists_actualJointProblem line 355
13. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.jointPolynomialOrbit line 449
14. abbrev OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.quotientFiltration line 463
15. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.QuotientFactors line 471
16. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.projectedData line 515
17. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.assembleQuotientFactors line 543
18. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.CommonFactors.toQuotientFactors line 586
19. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.ActualAdaptedPivotQuotientFactors line 696
20. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.CommonFactors.toActualAdaptedPivotQuotientFactors line 763
21. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedExternalCandidateSpatialNativeFamily_actual_adapted_quotient_factors line 805
22. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.ActualAdaptedPivotQuotientLongFactors line 999
23. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.longJointOrbit_polynomialCoordinates line 1071
24. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.LongCommonFactors.toActualAdaptedPivotQuotientLongFactors line 1089
25. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedExternalCandidateSpatialNativeFamily_actual_adapted_long_quotient_factors line 1195
26. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedExternalCandidateSpatialNativeFamily_native_long_geometry_factors line 1329