Commit 2024-08-21 15:34 9dc25c20

View on Github →

chore(Data/Nat/Choose/Sum): clean up (#15935)

Estimated changes

Modified Mathlib/Data/Nat/Choose/Sum.lean

modified theorem Nat.choose_middle_le_pow

modified theorem Nat.sum_range_choose

modified theorem Nat.sum_range_choose_halfway