Theorem Nat.choose_le_pow

Modification history

2024-09-02 07:21
Mathlib/Data/Nat/Choose/Bounds.lean
feat: remove completeness assumption in the formula for `∑ n, n * r ^ n` (#15270) …
Modified Nat.choose_le_powView on Github →
2023-07-19 05:37
Mathlib/Data/Nat/Choose/Bounds.lean
chore: cleanup whitespace (#5988) …
Modified Nat.choose_le_powView on Github →
2022-12-21 16:29
Mathlib/Data/Nat/Choose/Bounds.lean
feat: port data.nat.choose.bounds (#1139) …
Added Nat.choose_le_powView on Github →