OAI/NumberTheory/Ostmann/Arithmetic/MovingReducedPair.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The two original histories with a common regular-prime block extracted

  1. theorem OAI.Ostmann.movingOriginalGiantWeight_reduced_pair_factor line 11