Commit 2026-09-14 16:40 9cb3970b

refactor(Data/Nat/Choose/Central): move and rename four_pow_le_two_mul_add_one_mul_central_binom (#42606) Move four_pow_le_two_mul_add_one_mul_central_binom from Mathlib.Data.Nat.Choose.Sum to Mathlib.Data.Nat.Choose.Central and adjust it to fit the file's API:

• Rename: four_pow_le_two_mul_add_one_mul_central_binom → four_pow_le_two_mul_add_one_mul_centralBinom (aligning with centralBinom casing convention).
• Statement: Stated using centralBinom n rather than (2 * n).choose n.
• Proof: Simplified by using four_pow_le_two_mul_self_mul_centralBinom directly, avoiding an import dependency on Choose.Sum.
• Deprecation: Added a deprecation alias for the old name.