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

…7119)

A couple of lemmas that I needed for `det_vandermonde` (#7116).

I put them in a new file because I didn't see any obvious point that they fit in the import hierarchy. `big_operators/basic.lean` would be the alternative, but that file is big enough as it is.



Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

src/algebra/big_operators/fin.lean

@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2021 Anne Baanen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anne Baanen
+-/
+import algebra.big_operators.basic
+import data.fintype.fin
+/-!
+# Big operators and `fin`
+
+Some results about products and sums over the type `fin`.
+-/
+
+open_locale big_operators
+
+open finset
+
+namespace fin
+
+-- `to_additive` version of `prod_filter_zero_lt`, can't be autogenerated because
+-- of the `0` in the statement
+lemma sum_filter_zero_lt {M : Type*} [add_comm_monoid M] {n : ℕ} {v : fin n.succ → M} :
+  ∑ i in univ.filter (λ (i : fin n.succ), 0 < i), v i = ∑ (j : fin n), v j.succ :=
+by rw [univ_filter_zero_lt, sum_map, rel_embedding.coe_fn_to_embedding, coe_succ_embedding]
+
+@[to_additive]
+lemma prod_filter_zero_lt {M : Type*} [comm_monoid M] {n : ℕ} {v : fin n.succ → M} :
+  ∏ i in univ.filter (λ (i : fin n.succ), 0 < i), v i = ∏ (j : fin n), v j.succ :=
+by rw [univ_filter_zero_lt, finset.prod_map, rel_embedding.coe_fn_to_embedding, coe_succ_embedding]
+
+-- `to_additive` version of `prod_filter_succ_lt`, can't be autogenerated because
+-- of a `1` appearing in the proof
+lemma sum_filter_succ_lt {M : Type*} [add_comm_monoid M] {n : ℕ} (j : fin n) (v : fin n.succ → M) :
+  ∑ i in univ.filter (λ i, j.succ < i), v i =
+    ∑ j in univ.filter (λ i, j < i), v j.succ :=
+by rw [univ_filter_succ_lt, finset.sum_map, rel_embedding.coe_fn_to_embedding, coe_succ_embedding]
+
+@[to_additive]
+lemma prod_filter_succ_lt {M : Type*} [comm_monoid M] {n : ℕ} (j : fin n) (v : fin n.succ → M) :
+  ∏ i in univ.filter (λ i, j.succ < i), v i =
+    ∏ j in univ.filter (λ i, j < i), v j.succ :=
+by rw [univ_filter_succ_lt, finset.prod_map, rel_embedding.coe_fn_to_embedding, coe_succ_embedding]
+
+end fin

src/data/fintype/fin.lean

@@ -0,0 +1,54 @@
+/-
+Copyright (c) 2021 Anne Baanen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anne Baanen
+-/
+import data.fin
+import data.fintype.basic
+/-!
+# The structure of `fintype (fin n)`
+
+This file contains some basic results about the `fintype` instance for `fin`,
+especially properties of `finset.univ : finset (fin n)`.
+-/
+
+
+open finset
+open fintype
+
+namespace fin
+
+@[simp]
+lemma univ_filter_zero_lt {n : ℕ} :
+  (univ : finset (fin n.succ)).filter (λ i, 0 < i) =
+    univ.map (fin.succ_embedding _).to_embedding :=
+begin
+  ext i,
+  simp only [mem_filter, mem_map, mem_univ, true_and,
+  function.embedding.coe_fn_mk, exists_true_left],
+  split,
+  { refine cases _ _ i,
+    { rintro ⟨⟨⟩⟩ },
+    { intros i _, exact ⟨i, mem_univ _, rfl⟩ } },
+  { rintro ⟨i, _, rfl⟩,
+    exact succ_pos _ },
+end
+
+@[simp]
+lemma univ_filter_succ_lt {n : ℕ} (j : fin n) :
+  (univ : finset (fin n.succ)).filter (λ i, j.succ < i) =
+    (univ.filter (λ i, j < i)).map (fin.succ_embedding _).to_embedding :=
+begin
+  ext i,
+  simp only [mem_filter, mem_map, mem_univ, true_and,
+  function.embedding.coe_fn_mk, exists_true_left],
+  split,
+  { refine cases _ _ i,
+    { rintro ⟨⟨⟩⟩ },
+    { intros i hi,
+      exact ⟨i, mem_filter.mpr ⟨mem_univ _, succ_lt_succ_iff.mp hi⟩, rfl⟩ } },
+  { rintro ⟨i, hi, rfl⟩,
+    exact succ_lt_succ_iff.mpr (mem_filter.mp hi).2 },
+end
+
+end fin