Mathlib v3 is deprecated. Go to Mathlib v4

Theorem fin.Ioi_succ

Modification history

2022-07-26 02:21

src/data/fintype/fin.lean

feat(big_operators/fin): sum over elements of vector equal to `a` equals count `a` (#15360) …

Modified fin.Ioi_succ View on Github →

2022-06-26 00:12

src/data/fintype/fin.lean

refactor(*): Use `finset.Iix`/`finset.Ixi` (#14448) …

Added fin.Ioi_succ View on Github →