OAI/NumberTheory/Ostmann/Construction/TransferAdditiveProduct.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The complete additive phase after a transfer, on the actual prime list

  1. def OAI.Ostmann.transferredAdditiveRow line 16
  2. theorem OAI.Ostmann.transfer_additive_product line 24