OAI/NumberTheory/DukePrimeDegree/Entropy/RemainingConditionalIdentification.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Identifying a product factor from conditionals in the opposite root order

  1. theorem OAI.DukePrimeDegree.InitialRootStep.identify_remaining_conditional_factor line 14