Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+βCtrl+βto navigate, Ctrl+π±οΈto focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Aaron Anderson

! This file was ported from Lean 3 source module algebra.big_operators.nat_antidiagonal
! leanprover-community/mathlib commit 008205aa645b3f194c1da47025c5f110c8406eab
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Finset.NatAntidiagonal
import Mathlib.Algebra.BigOperators.Basic

/-!
# Big operators for `NatAntidiagonal`

This file contains theorems relevant to big operators over `Finset.NatAntidiagonal`.
-/

open BigOperators

variable {M: Type ?u.4904M N: Type ?u.1347N : Type _: Type (?u.1344+1)Type _} [CommMonoid: Type ?u.6201 β Type ?u.6201CommMonoid M: Type ?u.2M] [AddCommMonoid: Type ?u.4630 β Type ?u.4630AddCommMonoid N: Type ?u.5N]

namespace Finset

namespace Nat

theorem prod_antidiagonal_succ: β {n : β} {f : β Γ β β M}, β p in antidiagonal (n + 1), f p = f (0, n + 1) * β p in antidiagonal n, f (p.fst + 1, p.snd)prod_antidiagonal_succ {n: βn : β: Typeβ} {f: β Γ β β Mf : β: Typeβ Γ β: Typeβ β M: Type ?u.14M} :
(β p: ?m.99p in antidiagonal: β β Finset (β Γ β)antidiagonal (n: βn + 1: ?m.451), f: β Γ β β Mf p: ?m.99p) = f: β Γ β β Mf (0: ?m.1340, n: βn + 1: ?m.1441) * β p: ?m.187p in antidiagonal: β β Finset (β Γ β)antidiagonal n: βn, f: β Γ β β Mf (p: ?m.187p.1: {Ξ± : Type ?u.197} β {Ξ² : Type ?u.196} β Ξ± Γ Ξ² β Ξ±1 + 1: ?m.2011, p: ?m.187p.2: {Ξ± : Type ?u.243} β {Ξ² : Type ?u.242} β Ξ± Γ Ξ² β Ξ²2) :=
byGoals accomplished! π M: Type u_1N: Type ?u.17instβΒΉ: CommMonoid Minstβ: AddCommMonoid Nn: βf: β Γ β β Mβ p in antidiagonal (n + 1), f p = f (0, n + 1) * β p in antidiagonal n, f (p.fst + 1, p.snd)rw [M: Type u_1N: Type ?u.17instβΒΉ: CommMonoid Minstβ: AddCommMonoid Nn: βf: β Γ β β Mβ p in antidiagonal (n + 1), f p = f (0, n + 1) * β p in antidiagonal n, f (p.fst + 1, p.snd)antidiagonal_succ: β (n : β),
antidiagonal (n + 1) =     cons (0, n + 1)
(map (Function.Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Function.Embedding.refl β))
(antidiagonal n))
(_ :
Β¬(0, n + 1) β             map
(Function.Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Function.Embedding.refl β))
(antidiagonal n))antidiagonal_succ,M: Type u_1N: Type ?u.17instβΒΉ: CommMonoid Minstβ: AddCommMonoid Nn: βf: β Γ β β Mβ p in
cons (0, n + 1)
(map (Function.Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Function.Embedding.refl β))
(antidiagonal n))
(_ :
Β¬(0, n + 1) β             map
(Function.Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Function.Embedding.refl β))
(antidiagonal n)),
f p =   f (0, n + 1) * β p in antidiagonal n, f (p.fst + 1, p.snd) M: Type u_1N: Type ?u.17instβΒΉ: CommMonoid Minstβ: AddCommMonoid Nn: βf: β Γ β β Mβ p in antidiagonal (n + 1), f p = f (0, n + 1) * β p in antidiagonal n, f (p.fst + 1, p.snd)prod_cons: β {Ξ² : Type ?u.1074} {Ξ± : Type ?u.1073} {s : Finset Ξ±} {a : Ξ±} {f : Ξ± β Ξ²} [inst : CommMonoid Ξ²] (h : Β¬a β s),
β x in cons a s h, f x = f a * β x in s, f xprod_cons,M: Type u_1N: Type ?u.17instβΒΉ: CommMonoid Minstβ: AddCommMonoid Nn: βf: β Γ β β Mf (0, n + 1) *     β x in
map (Function.Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Function.Embedding.refl β))
(antidiagonal n),
f x =   f (0, n + 1) * β p in antidiagonal n, f (p.fst + 1, p.snd) M: Type u_1N: Type ?u.17instβΒΉ: CommMonoid Minstβ: AddCommMonoid Nn: βf: β Γ β β Mβ p in antidiagonal (n + 1), f p = f (0, n + 1) * β p in antidiagonal n, f (p.fst + 1, p.snd)prod_map: β {Ξ² : Type ?u.1204} {Ξ± : Type ?u.1203} {Ξ³ : Type ?u.1202} [inst : CommMonoid Ξ²] (s : Finset Ξ±) (e : Ξ± βͺ Ξ³) (f : Ξ³ β Ξ²),
β x in map e s, f x = β x in s, f (βe x)prod_mapM: Type u_1N: Type ?u.17instβΒΉ: CommMonoid Minstβ: AddCommMonoid Nn: βf: β Γ β β Mf (0, n + 1) *     β x in antidiagonal n,
f
(β(Function.Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Function.Embedding.refl β))
x) =   f (0, n + 1) * β p in antidiagonal n, f (p.fst + 1, p.snd)]M: Type u_1N: Type ?u.17instβΒΉ: CommMonoid Minstβ: AddCommMonoid Nn: βf: β Γ β β Mf (0, n + 1) *     β x in antidiagonal n,
f
(β(Function.Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Function.Embedding.refl β))
x) =   f (0, n + 1) * β p in antidiagonal n, f (p.fst + 1, p.snd);M: Type u_1N: Type ?u.17instβΒΉ: CommMonoid Minstβ: AddCommMonoid Nn: βf: β Γ β β Mf (0, n + 1) *     β x in antidiagonal n,
f
(β(Function.Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Function.Embedding.refl β))
x) =   f (0, n + 1) * β p in antidiagonal n, f (p.fst + 1, p.snd) M: Type u_1N: Type ?u.17instβΒΉ: CommMonoid Minstβ: AddCommMonoid Nn: βf: β Γ β β Mβ p in antidiagonal (n + 1), f p = f (0, n + 1) * β p in antidiagonal n, f (p.fst + 1, p.snd)rflGoals accomplished! π
#align finset.nat.prod_antidiagonal_succ Finset.Nat.prod_antidiagonal_succ: β {M : Type u_1} [inst : CommMonoid M] {n : β} {f : β Γ β β M},
β p in antidiagonal (n + 1), f p = f (0, n + 1) * β p in antidiagonal n, f (p.fst + 1, p.snd)Finset.Nat.prod_antidiagonal_succ

theorem sum_antidiagonal_succ: β {n : β} {f : β Γ β β N}, β p in antidiagonal (n + 1), f p = f (0, n + 1) + β p in antidiagonal n, f (p.fst + 1, p.snd)sum_antidiagonal_succ {n: βn : β: Typeβ} {f: β Γ β β Nf : β: Typeβ Γ β: Typeβ β N: Type ?u.1347N} :
(β p: ?m.1429p in antidiagonal: β β Finset (β Γ β)antidiagonal (n: βn + 1: ?m.13751), f: β Γ β β Nf p: ?m.1429p) = f: β Γ β β Nf (0: ?m.14620, n: βn + 1: ?m.14721) + β p: ?m.1515p in antidiagonal: β β Finset (β Γ β)antidiagonal n: βn, f: β Γ β β Nf (p: ?m.1515p.1: {Ξ± : Type ?u.1525} β {Ξ² : Type ?u.1524} β Ξ± Γ Ξ² β Ξ±1 + 1: ?m.15291, p: ?m.1515p.2: {Ξ± : Type ?u.1571} β {Ξ² : Type ?u.1570} β Ξ± Γ Ξ² β Ξ²2) :=
@prod_antidiagonal_succ: β {M : Type ?u.2309} [inst : CommMonoid M] {n : β} {f : β Γ β β M},
β p in antidiagonal (n + 1), f p = f (0, n + 1) * β p in antidiagonal n, f (p.fst + 1, p.snd)prod_antidiagonal_succ (Multiplicative: Type ?u.2310 β Type ?u.2310Multiplicative N: Type ?u.1347N) _ _: β_ _: β Γ β β Multiplicative N_
#align finset.nat.sum_antidiagonal_succ Finset.Nat.sum_antidiagonal_succ: β {N : Type u_1} [inst : AddCommMonoid N] {n : β} {f : β Γ β β N},
β p in antidiagonal (n + 1), f p = f (0, n + 1) + β p in antidiagonal n, f (p.fst + 1, p.snd)Finset.Nat.sum_antidiagonal_succ

@[to_additive: β {M : Type u_1} [inst : AddCommMonoid M] {n : β} {f : β Γ β β M},
β p in antidiagonal n, f (Prod.swap p) = β p in antidiagonal n, f pto_additive]
theorem prod_antidiagonal_swap: β {M : Type u_1} [inst : CommMonoid M] {n : β} {f : β Γ β β M},
β p in antidiagonal n, f (Prod.swap p) = β p in antidiagonal n, f pprod_antidiagonal_swap {n: βn : β: Typeβ} {f: β Γ β β Mf : β: Typeβ Γ β: Typeβ β M: Type ?u.4621M} :
(β p: ?m.4650p in antidiagonal: β β Finset (β Γ β)antidiagonal n: βn, f: β Γ β β Mf p: ?m.4650p.swap: {Ξ± : Type ?u.4653} β {Ξ² : Type ?u.4652} β Ξ± Γ Ξ² β Ξ² Γ Ξ±swap) = β p: ?m.4683p in antidiagonal: β β Finset (β Γ β)antidiagonal n: βn, f: β Γ β β Mf p: ?m.4683p := byGoals accomplished! π
M: Type u_1N: Type ?u.4624instβΒΉ: CommMonoid Minstβ: AddCommMonoid Nn: βf: β Γ β β Mβ p in antidiagonal n, f (Prod.swap p) = β p in antidiagonal n, f pconv_lhs => M: Type u_1N: Type ?u.4624instβΒΉ: CommMonoid Minstβ: AddCommMonoid Nn: βf: β Γ β β Mβ p in antidiagonal n, f (Prod.swap p) = β p in antidiagonal n, f prw [M: Type u_1N: Type ?u.4624instβΒΉ: CommMonoid Minstβ: AddCommMonoid Nn: βf: β Γ β β Mβ p in antidiagonal n, f (Prod.swap p)β map_swap_antidiagonal: β {n : β}, map { toFun := Prod.swap, inj' := (_ : Function.Injective Prod.swap) } (antidiagonal n) = antidiagonal nmap_swap_antidiagonal,M: Type u_1N: Type ?u.4624instβΒΉ: CommMonoid Minstβ: AddCommMonoid Nn: βf: β Γ β β Mβ p in map { toFun := Prod.swap, inj' := (_ : Function.Injective Prod.swap) } (antidiagonal n), f (Prod.swap p) M: Type u_1N: Type ?u.4624instβΒΉ: CommMonoid Minstβ: AddCommMonoid Nn: βf: β Γ β β Mβ p in antidiagonal n, f (Prod.swap p)Finset.prod_map: β {Ξ² : Type ?u.4736} {Ξ± : Type ?u.4735} {Ξ³ : Type ?u.4734} [inst : CommMonoid Ξ²] (s : Finset Ξ±) (e : Ξ± βͺ Ξ³) (f : Ξ³ β Ξ²),
β x in map e s, f x = β x in s, f (βe x)Finset.prod_mapM: Type u_1N: Type ?u.4624instβΒΉ: CommMonoid Minstβ: AddCommMonoid Nn: βf: β Γ β β Mβ x in antidiagonal n, f (Prod.swap (β{ toFun := Prod.swap, inj' := (_ : Function.Injective Prod.swap) } x))]M: Type u_1N: Type ?u.4624instβΒΉ: CommMonoid Minstβ: AddCommMonoid Nn: βf: β Γ β β Mβ x in antidiagonal n, f (Prod.swap (β{ toFun := Prod.swap, inj' := (_ : Function.Injective Prod.swap) } x))
#align finset.nat.prod_antidiagonal_swap Finset.Nat.prod_antidiagonal_swap: β {M : Type u_1} [inst : CommMonoid M] {n : β} {f : β Γ β β M},
β p in antidiagonal n, f (Prod.swap p) = β p in antidiagonal n, f pFinset.Nat.prod_antidiagonal_swap
#align finset.nat.sum_antidiagonal_swap Finset.Nat.sum_antidiagonal_swap: β {M : Type u_1} [inst : AddCommMonoid M] {n : β} {f : β Γ β β M},
β p in antidiagonal n, f (Prod.swap p) = β p in antidiagonal n, f pFinset.Nat.sum_antidiagonal_swap

theorem prod_antidiagonal_succ': β {n : β} {f : β Γ β β M}, β p in antidiagonal (n + 1), f p = f (n + 1, 0) * β p in antidiagonal n, f (p.fst, p.snd + 1)prod_antidiagonal_succ' {n: βn : β: Typeβ} {f: β Γ β β Mf : β: Typeβ Γ β: Typeβ β M: Type ?u.4904M} : (β p: ?m.4989p in antidiagonal: β β Finset (β Γ β)antidiagonal (n: βn + 1: ?m.49351), f: β Γ β β Mf p: ?m.4989p) =
f: β Γ β β Mf (n: βn + 1: ?m.50271, 0: ?m.50640) * β p: ?m.5077p in antidiagonal: β β Finset (β Γ β)antidiagonal n: βn, f: β Γ β β Mf (p: ?m.5077p.1: {Ξ± : Type ?u.5084} β {Ξ² : Type ?u.5083} β Ξ± Γ Ξ² β Ξ±1, p: ?m.5077p.2: {Ξ± : Type ?u.5091} β {Ξ² : Type ?u.5090} β Ξ± Γ Ξ² β Ξ²2 + 1: ?m.50951) := byGoals accomplished! π
M: Type u_1N: Type ?u.4907instβΒΉ: CommMonoid Minstβ: AddCommMonoid Nn: βf: β Γ β β Mβ p in antidiagonal (n + 1), f p = f (n + 1, 0) * β p in antidiagonal n, f (p.fst, p.snd + 1)rw [M: Type u_1N: Type ?u.4907instβΒΉ: CommMonoid Minstβ: AddCommMonoid Nn: βf: β Γ β β Mβ p in antidiagonal (n + 1), f p = f (n + 1, 0) * β p in antidiagonal n, f (p.fst, p.snd + 1)β prod_antidiagonal_swap: β {M : Type ?u.5953} [inst : CommMonoid M] {n : β} {f : β Γ β β M},
β p in antidiagonal n, f (Prod.swap p) = β p in antidiagonal n, f pprod_antidiagonal_swap,M: Type u_1N: Type ?u.4907instβΒΉ: CommMonoid Minstβ: AddCommMonoid Nn: βf: β Γ β β Mβ p in antidiagonal (n + 1), f (Prod.swap p) = f (n + 1, 0) * β p in antidiagonal n, f (p.fst, p.snd + 1) M: Type u_1N: Type ?u.4907instβΒΉ: CommMonoid Minstβ: AddCommMonoid Nn: βf: β Γ β β Mβ p in antidiagonal (n + 1), f p = f (n + 1, 0) * β p in antidiagonal n, f (p.fst, p.snd + 1)prod_antidiagonal_succ: β {M : Type ?u.6029} [inst : CommMonoid M] {n : β} {f : β Γ β β M},
β p in antidiagonal (n + 1), f p = f (0, n + 1) * β p in antidiagonal n, f (p.fst + 1, p.snd)prod_antidiagonal_succ,M: Type u_1N: Type ?u.4907instβΒΉ: CommMonoid Minstβ: AddCommMonoid Nn: βf: β Γ β β Mf (Prod.swap (0, n + 1)) * β p in antidiagonal n, f (Prod.swap (p.fst + 1, p.snd)) =   f (n + 1, 0) * β p in antidiagonal n, f (p.fst, p.snd + 1) M: Type u_1N: Type ?u.4907instβΒΉ: CommMonoid Minstβ: AddCommMonoid Nn: βf: β Γ β β Mβ p in antidiagonal (n + 1), f p = f (n + 1, 0) * β p in antidiagonal n, f (p.fst, p.snd + 1)β prod_antidiagonal_swap: β {M : Type ?u.6085} [inst : CommMonoid M] {n : β} {f : β Γ β β M},
β p in antidiagonal n, f (Prod.swap p) = β p in antidiagonal n, f pprod_antidiagonal_swapM: Type u_1N: Type ?u.4907instβΒΉ: CommMonoid Minstβ: AddCommMonoid Nn: βf: β Γ β β Mf (Prod.swap (0, n + 1)) * β p in antidiagonal n, f (Prod.swap ((Prod.swap p).fst + 1, (Prod.swap p).snd)) =   f (n + 1, 0) * β p in antidiagonal n, f (p.fst, p.snd + 1)]M: Type u_1N: Type ?u.4907instβΒΉ: CommMonoid Minstβ: AddCommMonoid Nn: βf: β Γ β β Mf (Prod.swap (0, n + 1)) * β p in antidiagonal n, f (Prod.swap ((Prod.swap p).fst + 1, (Prod.swap p).snd)) =   f (n + 1, 0) * β p in antidiagonal n, f (p.fst, p.snd + 1)
M: Type u_1N: Type ?u.4907instβΒΉ: CommMonoid Minstβ: AddCommMonoid Nn: βf: β Γ β β Mβ p in antidiagonal (n + 1), f p = f (n + 1, 0) * β p in antidiagonal n, f (p.fst, p.snd + 1)rflGoals accomplished! π
#align finset.nat.prod_antidiagonal_succ' Finset.Nat.prod_antidiagonal_succ': β {M : Type u_1} [inst : CommMonoid M] {n : β} {f : β Γ β β M},
β p in antidiagonal (n + 1), f p = f (n + 1, 0) * β p in antidiagonal n, f (p.fst, p.snd + 1)Finset.Nat.prod_antidiagonal_succ'

theorem sum_antidiagonal_succ': β {n : β} {f : β Γ β β N}, β p in antidiagonal (n + 1), f p = f (n + 1, 0) + β p in antidiagonal n, f (p.fst, p.snd + 1)sum_antidiagonal_succ' {n: βn : β: Typeβ} {f: β Γ β β Nf : β: Typeβ Γ β: Typeβ β N: Type ?u.6198N} :
(β p: ?m.6280p in antidiagonal: β β Finset (β Γ β)antidiagonal (n: βn + 1: ?m.62261), f: β Γ β β Nf p: ?m.6280p) = f: β Γ β β Nf (n: βn + 1: ?m.63161, 0: ?m.63530) + β p: ?m.6366p in antidiagonal: β β Finset (β Γ β)antidiagonal n: βn, f: β Γ β β Nf (p: ?m.6366p.1: {Ξ± : Type ?u.6373} β {Ξ² : Type ?u.6372} β Ξ± Γ Ξ² β Ξ±1, p: ?m.6366p.2: {Ξ± : Type ?u.6380} β {Ξ² : Type ?u.6379} β Ξ± Γ Ξ² β Ξ²2 + 1: ?m.63841) :=
@prod_antidiagonal_succ': β {M : Type ?u.7160} [inst : CommMonoid M] {n : β} {f : β Γ β β M},
β p in antidiagonal (n + 1), f p = f (n + 1, 0) * β p in antidiagonal n, f (p.fst, p.snd + 1)prod_antidiagonal_succ' (Multiplicative: Type ?u.7161 β Type ?u.7161Multiplicative N: Type ?u.6198N) _ _: β_ _: β Γ β β Multiplicative N_
#align finset.nat.sum_antidiagonal_succ' Finset.Nat.sum_antidiagonal_succ': β {N : Type u_1} [inst : AddCommMonoid N] {n : β} {f : β Γ β β N},
β p in antidiagonal (n + 1), f p = f (n + 1, 0) + β p in antidiagonal n, f (p.fst, p.snd + 1)Finset.Nat.sum_antidiagonal_succ'

@[to_additive: β {M : Type u_1} [inst : AddCommMonoid M] {n : β} {f : β Γ β β β β M},
β p in antidiagonal n, f p n = β p in antidiagonal n, f p (p.fst + p.snd)to_additive]
theorem prod_antidiagonal_subst: β {M : Type u_1} [inst : CommMonoid M] {n : β} {f : β Γ β β β β M},
β p in antidiagonal n, f p n = β p in antidiagonal n, f p (p.fst + p.snd)prod_antidiagonal_subst {n: βn : β: Typeβ} {f: β Γ β β β β Mf : β: Typeβ Γ β: Typeβ β β: Typeβ β M: Type ?u.9472M} :
(β p: ?m.9503p in antidiagonal: β β Finset (β Γ β)antidiagonal n: βn, f: β Γ β β β β Mf p: ?m.9503p n: βn) = β p: ?m.9527p in antidiagonal: β β Finset (β Γ β)antidiagonal n: βn, f: β Γ β β β β Mf p: ?m.9527p (p: ?m.9527p.1: {Ξ± : Type ?u.9533} β {Ξ² : Type ?u.9532} β Ξ± Γ Ξ² β Ξ±1 + p: ?m.9527p.2: {Ξ± : Type ?u.9539} β {Ξ² : Type ?u.9538} β Ξ± Γ Ξ² β Ξ²2) :=
prod_congr: β {Ξ² : Type ?u.9586} {Ξ± : Type ?u.9585} {sβ sβ : Finset Ξ±} {f g : Ξ± β Ξ²} [inst : CommMonoid Ξ²],
sβ = sβ β (β (x : Ξ±), x β sβ β f x = g x) β Finset.prod sβ f = Finset.prod sβ gprod_congr rfl: β {Ξ± : Sort ?u.9630} {a : Ξ±}, a = arfl fun p: ?m.9637p hp: ?m.9640hp β¦ byGoals accomplished! π M: Type u_1N: Type ?u.9475instβΒΉ: CommMonoid Minstβ: AddCommMonoid Nn: βf: β Γ β β β β Mp: β Γ βhp: p β antidiagonal nf p n = f p (p.fst + p.snd)rw [M: Type u_1N: Type ?u.9475instβΒΉ: CommMonoid Minstβ: AddCommMonoid Nn: βf: β Γ β β β β Mp: β Γ βhp: p β antidiagonal nf p n = f p (p.fst + p.snd)Nat.mem_antidiagonal: β {n : β} {x : β Γ β}, x β antidiagonal n β x.fst + x.snd = nNat.mem_antidiagonal.1: β {a b : Prop}, (a β b) β a β b1 hp: p β antidiagonal nhpM: Type u_1N: Type ?u.9475instβΒΉ: CommMonoid Minstβ: AddCommMonoid Nn: βf: β Γ β β β β Mp: β Γ βhp: p β antidiagonal nf p n = f p n]Goals accomplished! π
#align finset.nat.prod_antidiagonal_subst Finset.Nat.prod_antidiagonal_subst: β {M : Type u_1} [inst : CommMonoid M] {n : β} {f : β Γ β β β β M},
β p in antidiagonal n, f p n = β p in antidiagonal n, f p (p.fst + p.snd)Finset.Nat.prod_antidiagonal_subst
#align finset.nat.sum_antidiagonal_subst Finset.Nat.sum_antidiagonal_subst: β {M : Type u_1} [inst : AddCommMonoid M] {n : β} {f : β Γ β β β β M},
β p in antidiagonal n, f p n = β p in antidiagonal n, f p (p.fst + p.snd)Finset.Nat.sum_antidiagonal_subst

@[to_additive: β {M : Type u_1} [inst : AddCommMonoid M] (f : β Γ β β M) (n : β),
β ij in antidiagonal n, f ij = β k in range (Nat.succ n), f (k, n - k)to_additive]
theorem prod_antidiagonal_eq_prod_range_succ_mk: β {M : Type u_1} [inst : CommMonoid M] (f : β Γ β β M) (n : β),
β ij in antidiagonal n, f ij = β k in range (Nat.succ n), f (k, n - k)prod_antidiagonal_eq_prod_range_succ_mk {M: Type ?u.9733M : Type _: Type (?u.9733+1)Type _} [CommMonoid: Type ?u.9736 β Type ?u.9736CommMonoid M: Type ?u.9733M] (f: β Γ β β Mf : β: Typeβ Γ β: Typeβ β M: Type ?u.9733M)
(n: βn : β: Typeβ) : (β ij: ?m.9756ij in Finset.Nat.antidiagonal: β β Finset (β Γ β)Finset.Nat.antidiagonal n: βn, f: β Γ β β Mf ij: ?m.9756ij) = β k: ?m.9781k in range: β β Finset βrange n: βn.succ: β β βsucc, f: β Γ β β Mf (k: ?m.9781k, n: βn - k: ?m.9781k) :=
Finset.prod_map: β {Ξ² : Type ?u.9841} {Ξ± : Type ?u.9840} {Ξ³ : Type ?u.9839} [inst : CommMonoid Ξ²] (s : Finset Ξ±) (e : Ξ± βͺ Ξ³) (f : Ξ³ β Ξ²),
β x in map e s, f x = β x in s, f (βe x)Finset.prod_map (range: β β Finset βrange n: βn.succ: β β βsucc) β¨fun i: ?m.9859i β¦ (i: ?m.9859i, n: βn - i: ?m.9859i), fun _: ?m.9904_ _: ?m.9907_ h: ?m.9910h β¦ (Prod.mk.inj: β {Ξ± : Type ?u.9913} {Ξ² : Type ?u.9912} {fst : Ξ±} {snd : Ξ²} {fst_1 : Ξ±} {snd_1 : Ξ²},
(fst, snd) = (fst_1, snd_1) β fst = fst_1 β§ snd = snd_1Prod.mk.inj h: ?m.9910h).1: β {a b : Prop}, a β§ b β a1β© f: β Γ β β Mf
#align finset.nat.prod_antidiagonal_eq_prod_range_succ_mk Finset.Nat.prod_antidiagonal_eq_prod_range_succ_mk: β {M : Type u_1} [inst : CommMonoid M] (f : β Γ β β M) (n : β),
β ij in antidiagonal n, f ij = β k in range (Nat.succ n), f (k, n - k)Finset.Nat.prod_antidiagonal_eq_prod_range_succ_mk
#align finset.nat.sum_antidiagonal_eq_sum_range_succ_mk Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk: β {M : Type u_1} [inst : AddCommMonoid M] (f : β Γ β β M) (n : β),
β ij in antidiagonal n, f ij = β k in range (Nat.succ n), f (k, n - k)Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk

/-- This lemma matches more generally than `Finset.Nat.prod_antidiagonal_eq_prod_range_succ_mk` when
using `rw β`. -/
@[to_additive: β {M : Type u_1} [inst : AddCommMonoid M] (f : β β β β M) (n : β),
β ij in antidiagonal n, f ij.fst ij.snd = β k in range (Nat.succ n), f k (n - k)to_additive "This lemma matches more generally than
`Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk` when using `rw β`."]
theorem prod_antidiagonal_eq_prod_range_succ: β {M : Type u_1} [inst : CommMonoid M] (f : β β β β M) (n : β),
β ij in antidiagonal n, f ij.fst ij.snd = β k in range (Nat.succ n), f k (n - k)prod_antidiagonal_eq_prod_range_succ {M: Type u_1M : Type _: Type (?u.10073+1)Type _} [CommMonoid: Type ?u.10076 β Type ?u.10076CommMonoid M: Type ?u.10073M] (f: β β β β Mf : β: Typeβ β β: Typeβ β M: Type ?u.10073M) (n: βn : β: Typeβ) :
(β ij: ?m.10096ij in Finset.Nat.antidiagonal: β β Finset (β Γ β)Finset.Nat.antidiagonal n: βn, f: β β β β Mf ij: ?m.10096ij.1: {Ξ± : Type ?u.10099} β {Ξ² : Type ?u.10098} β Ξ± Γ Ξ² β Ξ±1 ij: ?m.10096ij.2: {Ξ± : Type ?u.10105} β {Ξ² : Type ?u.10104} β Ξ± Γ Ξ² β Ξ²2) = β k: ?m.10131k in range: β β Finset βrange n: βn.succ: β β βsucc, f: β β β β Mf k: ?m.10131k (n: βn - k: ?m.10131k) :=
prod_antidiagonal_eq_prod_range_succ_mk: β {M : Type ?u.10183} [inst : CommMonoid M] (f : β Γ β β M) (n : β),
β ij in antidiagonal n, f ij = β k in range (Nat.succ n), f (k, n - k)prod_antidiagonal_eq_prod_range_succ_mk _: β Γ β β ?m.10184_ _: β_
#align finset.nat.prod_antidiagonal_eq_prod_range_succ Finset.Nat.prod_antidiagonal_eq_prod_range_succ: β {M : Type u_1} [inst : CommMonoid M] (f : β β β β M) (n : β),
β ij in antidiagonal n, f ij.fst ij.snd = β k in range (Nat.succ n), f k (n - k)Finset.Nat.prod_antidiagonal_eq_prod_range_succ
#align finset.nat.sum_antidiagonal_eq_sum_range_succ Finset.Nat.sum_antidiagonal_eq_sum_range_succ: β {M : Type u_1} [inst : AddCommMonoid M] (f : β β β β M) (n : β),
β ij in antidiagonal n, f ij.fst ij.snd = β k in range (Nat.succ n), f k (n - k)Finset.Nat.sum_antidiagonal_eq_sum_range_succ
end Nat

end Finset
```