OAI/NumberTheory/Ostmann/Arithmetic/MovingLineComposition.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Composition of the cleared occurrence lines

The identity works before any descendant division. It lets the current internal-prime congruence establish integrality inductively, without assuming the conclusion for the rest of the path.

  1. def OAI.Ostmann.PolynomialGiantRows.evalNumerator line 15
  2. theorem OAI.Ostmann.PolynomialGiantRows.evalNumerator_movingReverse line 19
  3. theorem OAI.Ostmann.movingPolynomialAncestors_append_eval line 29
  4. theorem OAI.Ostmann.PolynomialGiantRows.evalNumerator_smul line 42
  5. theorem OAI.Ostmann.movingSlotLine_eval line 48
  6. theorem OAI.Ostmann.movingSlotLine_append_singleton line 62

    Source documentation

    A root division multiplies every descendant cleared line by its root denominator. No integrality of the descendant path is needed.

    theorem movingSlotLine_append_singleton {σ R : Type*} [CommRing R]
    (φ : MvPolynomial σ ℤ →+* R) (path : List (MovingSlotReversal σ))
    (current root : MovingSlotReversal σ) (x y p : R)
    (hroot : φ root.polynomial.v * y - φ root.polynomial.w * x = φ root.polynomial.u * p) :
    φ (movingSlotLine (path ++ [root]) current).a * x +
        φ (movingSlotLine (path ++ [root]) current).b * y =
      φ root.polynomial.u * (φ (movingSlotLine path current).a * p +
        φ (movingSlotLine path current).b * (if root.left then x else y)) := by
…

    Mentions: OAI.Ostmann.MovingSlotReversal, OAI.Ostmann.movingSlotLine

  7. theorem OAI.Ostmann.movingSlotLine_append_singleton_zero_iff line 84