OAI/NumberTheory/Ostmann/Characters/PivotResidueGrouping.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Grouping the actual pivot row before the integer extension

  1. theorem OAI.Ostmann.pivot_residue_grouping line 12
  2. theorem OAI.Ostmann.pivot_grouped_integer_transfer line 21