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