mathlib documentation

algebra.big_operators.fin

Big operators and fin #

Some results about products and sums over the type fin.

theorem fin.sum_filter_zero_lt {M : Type u_1} [add_comm_monoid M] {n : } {v : fin n.succ → M} :
∑ (i : fin n.succ) in finset.filter (λ (i : fin n.succ), 0 < i) finset.univ, v i = ∑ (j : fin n), v j.succ
theorem fin.prod_filter_zero_lt {M : Type u_1} [comm_monoid M] {n : } {v : fin n.succ → M} :
∏ (i : fin n.succ) in finset.filter (λ (i : fin n.succ), 0 < i) finset.univ, v i = ∏ (j : fin n), v j.succ
theorem fin.sum_filter_succ_lt {M : Type u_1} [add_comm_monoid M] {n : } (j : fin n) (v : fin n.succ → M) :
∑ (i : fin n.succ) in finset.filter (λ (i : fin n.succ), j.succ < i) finset.univ, v i = ∑ (j : fin n) in finset.filter (λ (i : fin n), j < i) finset.univ, v j.succ
theorem fin.prod_filter_succ_lt {M : Type u_1} [comm_monoid M] {n : } (j : fin n) (v : fin n.succ → M) :
∏ (i : fin n.succ) in finset.filter (λ (i : fin n.succ), j.succ < i) finset.univ, v i = ∏ (j : fin n) in finset.filter (λ (i : fin n), j < i) finset.univ, v j.succ