1<!DOCTYPE html> 2<html lang="en"><head> 3 <meta charset="utf-8"> 4 <meta name="viewport" content="width=device-width, initial-scale=1"> 5 <title>Fast Chinese Remaindering via Product Trees - Archive of Formal Proofs</title> 6 <meta name="description" content="Fast Chinese Remaindering via Product Trees in the Archive of Formal Proofs"> 7 <meta property="og:description" content="Fast Chinese Remaindering via Product Trees in the Archive of Formal Proofs"> 8 <meta property="og:title" content="Fast Chinese Remaindering via Product Trees"> 9 <meta property="og:url" content="https://isa-afp.org/entries/CRT_Product_Tree.html"> 10 <meta property="og:image" content="https://isa-afp.org/images/afp.png"> 11 <meta property="og:type" content="article"> 12 <link rel="stylesheet" type="text/css" href="../css/front.min.css"> 13 <link rel="icon" href="../images/favicon.ico" type="image/icon"> 14 15
15<script> 16 MathJax = { 17 tex: { 18 inlineMath: [["$", "$"], ["\\(", "\\)"]] 19 }, 20 processEscapes: true, 21 svg: { 22 fontCache: "global" 23 } 24 }; 25 </script>
25 26
26<script id="MathJax-script" async src="../js/mathjax/es5/tex-mml-chtml.js"> 27 </script>
27 28 29
29<script src="../js/library.js"></script>
29 30
30<script src="../js/flexsearch.bundle.js"></script>
30 31
31<script src="../js/search-autocomplete.js"></script>
31 32
32<script src="../js/obfuscate.js"></script>
32 33
33<script src="../js/entries.js"></script>
33 34</head> 35 36 <body class="mathjax_ignore"> 37 <aside><div id="menu-toggle"> 38 <input id="toggle" type="checkbox"> 39 <label for="toggle"> 40 <span>menu</span> 41 <img src="../images/menu.svg" alt="Menu"> 42 </label> 43 <a href="../" class="logo-link"> 44 <img src="../images/afp.png" alt="Logo of the Archive of Formal Proofs" class="logo"> 45 </a> 46 <nav id="menu"> 47 <div> 48 <a href="../" class="logo-link"> 49 <img src="../images/afp.png" alt="Logo of the Archive of Formal Proofs" class="logo"> 50 </a> 51 <ul> 52 <li > 53 <a href="../">Home</a> 54 </li> 55 <li > 56 <a href="../topics/">Topics</a> 57 </li> 58 <li > 59 <a href="../download/">Download</a> 60 </li> 61 <li > 62 <a href="../help/">Help</a> 63 </li> 64 <li > 65 <a href="../submission/">Submission</a> 66 </li> 67 <li > 68 <a href="../statistics/">Statistics</a> 69 </li> 70 <li > 71 <a href="../about/">About</a> 72 </li> 73 </ul> 74 </div> 75 </nav> 76</div> 77 </aside> 78 79 <div class="content entries"><header> 80 <form autocomplete="off" action="../search/"> 81 <div class="form-container"> 82 <input id="search-input" name="s" type="search" size="31" maxlength="255" value="" 83 aria-label="Search the AFP" list="autocomplete"><button id="search-button" type="submit"> 84 <img src="../images/search.svg" alt="Search"> 85 </button> 86 <datalist id="autocomplete"></datalist> 87 </div> 88 </form> 89 <h1> 90 <span class='first'>F</span>ast <span class='first'>C</span>hinese <span class='first'>R</span>emaindering via <span class='first'>P</span>roduct <span class='first'>T</span>rees 91 </h1> 92 <div> 93 <p><a href="../authors/eberl/">Manuel Eberl</a> <a class="obfuscated" data="eyJ1c2VyIjpbIm1hbnVlbCJdLCJob3N0IjpbInBydXZpc3RvIiwib3JnIl19">ð§</a> 94 </p> 95 <p class="date">September 4, 2026</p> 96 </div> 97</header> 98 <div> 99 <main> 100 101 <h3>Abstract</h3> 102 <div class="abstract mathjax_process"><p>Product trees are a simple data structure that, broadly speaking, allows dealing with the product of a large number of (typically coprime) integers, or more generally elements of a Euclidean ring.</p> 103<p>This is particularly useful for efficient simultaneous modular reduction, i.e. computing $x\mathbin{\text{mod}} m_i$ for a large number of moduli $m_i$ at the same time for a fixed $x$, and the inverse operation thereof, i.e. modular reconstruction (also known as “Chinese Remaindering”).</p> 104<p>The algorithms formalised are adapted from the book <em><a href="https://doi.org/10.1017/CBO9781139856065">“Modern Computer Algebra”</a> by von zur Gathen and Gerhard.</p></div> 105 106 <h3>License</h3> 107 <div> 108 <a href="https://isa-afp.org/LICENSE">BSD License</a> 109 </div> 110 <h3>Topics</h3> 111 <ul> 112 <li><a href="../topics/mathematics/algebra/">Mathematics/Algebra</a></li> 113 </ul> 114 <h3>Session CRT_Product_Tree</h3> 115 <ul> 116 <li><a href="../thys/CRT_Product_Tree/CRT_Product_Tree.html">CRT_Product_Tree</a></li> 117 <li><a href="../thys/CRT_Product_Tree/CRT_Product_Tree_Benchmark.html">CRT_Product_Tree_Benchmark</a></li> 118 </ul> 119 120 <div class="flex-wrap"> 121 <div> 122 <h3>Similar entries</h3> 123 <ul class="horizontal-list"> 124 <li><a href="../entries/LLL_Basis_Reduction.html">A verified LLL algorithm</a></li> 125 </ul> 126 </div> 127 </div> 128 </main> 129 130 <nav class="links"> 131 <a class="popup-button" href="#cite-popup">Cite</a> 132 <a class="popup-button" href="#download-popup">Download</a> 133 <h4>PDFs</h4> 134 <a href="https://isa-afp.org/browser_info/current/AFP/CRT_Product_Tree/outline.pdf">Proof outline</a> 135 <a href="https://isa-afp.org/browser_info/current/AFP/CRT_Product_Tree/document.pdf">Proof document</a> 136 <a href="https://isa-afp.org/browser_info/current/AFP/CRT_Product_Tree/session_graph.pdf">Dependencies</a> 137 </nav> 138 139 <div id="cite-popup" class="overlay"> 140 <a class="cancel" href="#"></a> 141 <div class="popup"> 142 <h2>Cite</h2> 143 <a class="close" href="#">×</a> 144 <div> 145 <p style="display:none;" id="bibtex-filename">CRT_Product_Tree-AFP</p> 146 <pre id="copy-text">@article{CRT_Product_Tree-AFP, 147 author = {Manuel Eberl}, 148 title = {Fast Chinese Remaindering via Product Trees}, 149 journal = {Archive of Formal Proofs}, 150 month = {September}, 151 year = {2026}, 152 note = {\url{https://isa-afp.org/entries/CRT_Product_Tree.html}, 153 Formal proof development}, 154 ISSN = {2150-914x}, 155}</pre> 156 <button id="copy-bibtex">Copy</button> <a id="download-bibtex">Download</a> 157 </div> 158 </div> 159 </div> 160 161 <div id="download-popup" class="overlay"> 162 <a class="cancel" href="#"></a> 163 <div class="popup"> 164 <h2>Download</h2> 165 <a class="close" href="#">×</a> 166 <a href="https://isa-afp.org/release/afp-CRT_Product_Tree-current.tar.gz" download> 167 Download latest</a> 168 </div> 169 </div> 170 </div> 171 </div> 172 </body> 173</html>
Line numbers count LF bytes from the start of the resource, as the search results do. Vendor segments are library code the classifier recognised; they are stored but not indexed. Bytes are shown as Latin1 characters, one per byte.