The binomial theorem for the integers

module elementary-number-theory.binomial-theorem-integers where

open import commutative-algebra.binomial-theorem-commutative-rings

open import elementary-number-theory.addition-integers
open import elementary-number-theory.commutative-ring-of-integers
open import elementary-number-theory.distance-natural-numbers
open import elementary-number-theory.integers
open import elementary-number-theory.multiplication-integers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.powers-integers

open import foundation.homotopies
open import foundation.identity-types

open import linear-algebra.vectors

open import univalent-combinatorics.standard-finite-types

Idea

The binomial theorem for the integers asserts that for any two integers x and y and any natural number n, we have

  (x + y)ⁿ = ∑_{0 ≤ i < n+1} (n choose i) xⁱ yⁿ⁻ⁱ.

Definitions

Binomial sums

binomial-sum-ℤ : (n : ℕ) (f : functional-vec ℤ (succ-ℕ n)) → ℤ
binomial-sum-ℤ = binomial-sum-Commutative-Ring ℤ-Commutative-Ring

Properties

Binomial sums of one and two elements

binomial-sum-one-element-ℤ :
  (f : functional-vec ℤ ) → binomial-sum-ℤ  f ＝ head-functional-vec  f
binomial-sum-one-element-ℤ =
  binomial-sum-one-element-Commutative-Ring ℤ-Commutative-Ring

binomial-sum-two-elements-ℤ :
  (f : functional-vec ℤ ) →
  binomial-sum-ℤ  f ＝ (f (zero-Fin )) +ℤ (f (one-Fin ))
binomial-sum-two-elements-ℤ =
  binomial-sum-two-elements-Commutative-Ring ℤ-Commutative-Ring

Binomial sums are homotopy invariant

htpy-binomial-sum-ℤ :
  (n : ℕ) {f g : functional-vec ℤ (succ-ℕ n)} →
  (f ~ g) → binomial-sum-ℤ n f ＝ binomial-sum-ℤ n g
htpy-binomial-sum-ℤ =
  htpy-binomial-sum-Commutative-Ring ℤ-Commutative-Ring

Multiplication distributes over sums

left-distributive-mul-binomial-sum-ℤ :
  (n : ℕ) (x : ℤ) (f : functional-vec ℤ (succ-ℕ n)) →
  x *ℤ (binomial-sum-ℤ n f) ＝ binomial-sum-ℤ n (λ i → x *ℤ (f i))
left-distributive-mul-binomial-sum-ℤ =
  left-distributive-mul-binomial-sum-Commutative-Ring ℤ-Commutative-Ring

right-distributive-mul-binomial-sum-ℤ :
  (n : ℕ) (f : functional-vec ℤ (succ-ℕ n)) (x : ℤ) →
  (binomial-sum-ℤ n f) *ℤ x ＝ binomial-sum-ℤ n (λ i → (f i) *ℤ x)
right-distributive-mul-binomial-sum-ℤ =
  right-distributive-mul-binomial-sum-Commutative-Ring
    ℤ-Commutative-Ring

Theorem

Binomial theorem for the integers

binomial-theorem-ℤ :
  (n : ℕ) (x y : ℤ) →
  power-ℤ n (x +ℤ y) ＝
  binomial-sum-ℤ n
    ( λ i →
        ( power-ℤ (nat-Fin (succ-ℕ n) i) x) *ℤ
        ( power-ℤ (dist-ℕ (nat-Fin (succ-ℕ n) i) n) y))
binomial-theorem-ℤ = binomial-theorem-Commutative-Ring ℤ-Commutative-Ring