Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finset.prod_Ico_id_eq_fact

Modification history

2020-10-01 12:28
src/algebra/big_operators/intervals.lean
feat(data/nat/fact, analysis/specific_limits): rename nat.fact, add few lemmas about its behaviour along at_top (#4309) …
Deleted finset.prod_Ico_id_eq_factView on Github →
2020-07-22 10:18
src/algebra/big_operators/basic.lean
refactor(algebra/big_operators): split file, reduce imports (#3495) …
Modified finset.prod_Ico_id_eq_factView on Github →
2020-06-11 11:41
src/algebra/big_operators.lean
chore(*): use prod and sum notation (#3027)
Modified finset.prod_Ico_id_eq_factView on Github →
2020-05-02 15:22
src/algebra/big_operators.lean
refactor(algebra/big_operators): introduce notation for finset.prod and finset.sum (#2582) …
Modified finset.prod_Ico_id_eq_factView on Github →
2020-01-26 01:12
src/algebra/big_operators.lean
feat(*): some simple lemmas about sets and finite sets (#1903) …
Modified finset.prod_Ico_id_eq_factView on Github →
2019-11-10 19:42
src/algebra/big_operators.lean
refactor(data/zmod/quadratic_reciprocity): simplify proof of quadratic reciprocity and prove when 2 is a square (#1609) …
Added finset.prod_Ico_id_eq_factView on Github →