Sums and products over Fin n

Successive differences along a finite sequence sum to the difference of its endpoints, including the empty edge sequence. Reversing every difference reverses the endpoint difference. The equivalence omitting the last index also reindexes sums by the preceding indices.

Along a divisibility chain d₀ ∣ d₁ ∣ ⋯, the product of the first k entries divides the product of the entries at any k distinct positions. This is what makes the leading k × k minors of a diagonal matrix with chained entries the smallest ones in divisibility.

theorem Fin.sum_univ_succ_sub_castSucc {G : Type u_1} [AddCommGroup G] {n : ℕ} (f : Fin (n + 1) → G) : ∑ i : Fin n, (f i.succ - f i.castSucc) = f (last n) - f 0

Successive differences telescope to the endpoint difference.

theorem Fin.sum_univ_castSucc_sub_succ {G : Type u_1} [AddCommGroup G] {n : ℕ} (f : Fin (n + 1) → G) : ∑ i : Fin n, (f i.castSucc - f i.succ) = f 0 - f (last n)

Reversed successive differences telescope to the reversed endpoint difference.

theorem Fin.prod_castLE_dvd_prod_of_injective {M : Type u_1} [CommMonoid M] {n : ℕ} {d : Fin n → M} (hd : ∀ ⦃i j : Fin n⦄, i ≤ j → d i ∣ d j) {k : ℕ} (hk : k ≤ n) {f : Fin k → Fin n} (hf : Function.Injective f) : ∏ j : Fin k, d (castLE hk j) ∣ ∏ j : Fin k, d (f j)

The leading entries of a divisibility chain divide any equally many entries. Along a chain d₀ ∣ d₁ ∣ ⋯, the product of the first k entries divides the product of the entries at any k distinct positions.

theorem TauCeti.sum_finSuccAboveEquiv_last {M : Type u_1} [AddCommMonoid M] (n : ℕ) (z : { i : Fin (n + 1) // i ≠ Fin.last n } → M) : ∑ i : Fin n, z ⟨i.castSucc, ⋯⟩ = ∑ j : { i : Fin (n + 1) // i ≠ Fin.last n }, z j

Reindex a sum over all indices except the last by the preceding finite ordinal.