OAI/NumberTheory/Ostmann/Construction/FinitePivotSchedule.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite pivot hypotheses for a finite-depth arithmetic schedule

Only the pivots through the current depth occur in these formulas. The finite construction therefore supplies exactly those roles, without a hypothesis requiring infinitely many roles in a finite type.

  1. theorem OAI.Ostmann.scheduledRegularRow_pivot_finite line 14
  2. theorem OAI.Ostmann.copyScheduleUnary_pivot_finite line 38
  3. theorem OAI.Ostmann.scheduledRetainedGraph_pivot_column_finite line 79