OAI/Combinatorics/Progressions/Geometry/AllocatedExternalCandidateSpatialNativeLongCommonFactors.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.longJointOrbit line 51
2. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.LongCommonFactors line 60
3. theorem OAI.Erdos3.VectorPolynomial.compose_exponential_mass_losses line 96

   Also declared: OAI/Combinatorics/Progressions/Geometry/AllocatedExternalCandidateSpatialNativeAutomaticLongGeometry.lean:148 (same declaration text).

4. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedExternalCandidateSpatialNativeFamily_long_common_factors line 106