Mathlib v3 is deprecated. Go to Mathlib v4

Theorem fin.univ_filter_succ_lt

Modification history

2022-06-26 00:12

src/data/fintype/fin.lean

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

Deleted fin.univ_filter_succ_lt View on Github →

2021-04-14 23:14

src/data/fintype/fin.lean

feat(algebra/big_operators): some lemmas on big operators and `fin` (#7119) …

Added fin.univ_filter_succ_lt View on Github →