by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
We have v2(3101+5101)=v2(3+5)+v2(101)=3+0=3. If you don't know LTE: \nWe have 3101+5101=(3+5)(3100−3995+⋯+350550−⋯−5993+5100). The second term has an odd number of odd terms( 101 ), so it is odd. The only factors of 2 are in 3+5=8⟹3.