OAI/NumberTheory/DukePrimeDegree/Geometry/PrefixFactorIdentification.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Recovering the remaining factor from extended-prefix conditionals

  1. theorem OAI.DukePrimeDegree.InitialRootStep.identify_factor_from_extended_prefix line 15