OAI/NumberTheory/Ostmann/Arithmetic/ReconstructedCoprimalityBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Large-prime support after reconstruction

An identically divisible reconstructed numerator has empty valid support. Otherwise the original independent prime priors give the polynomial error. No conditioning of those priors is used in either case.

  1. theorem OAI.Ostmann.reconstructed_coprimality_bound line 15