Mathlib Changelog
v4
Changelog
About
Github
Theorem
Finset.lt_geomSum_of_mem
Modification history
2025-01-30 19:51
Mathlib/Combinatorics/Colex.lean
chore: deprecate the `∑ x in s, f x` notation (#21253) …
Modified
Finset.lt_geomSum_of_mem
View on Github →
2024-07-15 14:00
Mathlib/Combinatorics/Colex.lean
feat(Combinatorics/Colex): binary expansions give the colexicographic order on `Finset Nat` (#12346) …
Added
Finset.lt_geomSum_of_mem
View on Github →