Commit 2022-05-18 16:04 503970d2

View on Github →

chore(data/fintype/basic): Better fin lemmas (#14200) Turn finset.image into finset.map and insert into finset.cons in the three lemmas relating univ : finset (fin (n + 1)) and univ : finset (fin n). Golf proofs involving the related big operators lemmas.

Estimated changes

Modified src/algebra/big_operators/basic.lean

modified theorem finset.prod_empty

added theorem finset.prod_of_empty

Modified src/algebra/big_operators/fin.lean

added theorem fin.prod_cons

modified theorem fin.prod_univ_succ_above

Modified src/data/fin/tuple/nat_antidiagonal.lean

Modified src/data/fintype/basic.lean

Modified src/linear_algebra/linear_independent.lean