Factorization

Navigation page for Library/Factorization/ at upstream snapshot c141acfbb5ddf4d390e812cbb2e822aabbca09ad.

Contents

• Perfect powers and the Wall–Sun–Sun obstruction
• Bárcena-Petisco, Martínez, Merino, Montoya and Vera-López, greedy difference matrix
• Chebotarev density in Lean
• OEIS A152020
• Lucas square and twice-square classifications
• Cyclotomic extensions
• Inversion formulas and divisor Dirichlet series
• A shared chain for finite divisor factors
• Erdős’s consecutive-product factorization question
• The square-sided-dice midpoint assertion
• OEIS A092028
• OEIS A008474
• The A400168 existence question
• The ordinary Loopy polynomial and degree sequences with loops
• OEIS A302975
• Fibonacci and Lucas p-adic orders
• OEIS A225004
• Fibonacci rank descent and Pratt-Fibonacci trees
• Multiplicative divisor sums
• Finite geometric factors
• Reciprocal LCM powers: reuse the existing source and parameter criterion
• OEIS A096127
• Nikolov–Segal strong completeness and an abelian Lean precursor
• Classical prefix-lcm reconstruction
• OEIS A108569, fixed points of phi under the shift by phi
• OEIS A000224, squares modulo n
• OEIS A094802
• OEIS A400194
• Subspace-Theorems
• A375007
• Square-class rigidity and explicit original-depth support bounds
• OEIS A119623
• OEIS A363956
• An explicit CA window and its residual obstruction
• OEIS A258409
• OEIS A328959
• OEIS A062319