OAI/NumberTheory/Ostmann/Construction/ConstituentPivotEnumeration.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.pivotConstituentEquiv line 12

   Source documentation

   A single pivot atom contributes exactly its original number of prime constituents, even after the earlier copy steps.

   noncomputable def pivotConstituentEquiv {I : Type*}
       (role : I → CopyScheduleRole) (size : I → ℕ) (n : ℕ) (p : I)
       (hp : role p = .pivot n) (hu : ∀ i, role i = .pivot n → i = p) :
       Fin (size p) ≃ CurrentPivotConstituent (fun i : Σ a, Fin (size a) => role i.1) n :=
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CurrentPivotConstituent

2. def OAI.Ostmann.constituentPivot line 28

   Source documentation

   Choose the first prime constituent solely to name the pivot column. All constituents remain present in the grouped phase and prior.

   def constituentPivot {I : Type*} (size : I → ℕ) (pivot : ℕ → I)
       (hsize : ∀ n, 0 < size (pivot n)) (n : ℕ) : Σ i, Fin (size i) :=
   …

3. theorem OAI.Ostmann.constituentPivot_role line 32
4. theorem OAI.Ostmann.currentPivotConstituent_card line 37