OAI/NumberTheory/CubicMoment/Angular/AngularStoppedDivisorCube.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Small square divisors act on the actual nonzero stopped rows. Zero coefficients impose no artificial coprimality condition on the ambient support.

  1. lemma OAI.CubicFirstMoment.angular_stopped_active_coprime_small line 16
  2. lemma OAI.CubicFirstMoment.angular_stopped_divisor_cube_eq line 35