The binomial theorem for the natural numbers

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2023-02-20.
Last modified on 2024-10-29.

module elementary-number-theory.binomial-theorem-natural-numbers where
Imports 
open import commutative-algebra.binomial-theorem-commutative-semirings

open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.commutative-semiring-of-natural-numbers
open import elementary-number-theory.distance-natural-numbers
open import elementary-number-theory.exponentiation-natural-numbers
open import elementary-number-theory.multiplication-natural-numbers
open import elementary-number-theory.natural-numbers

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 natural numbers asserts that for any two natural numbers x and y and any natural number n, we have

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

The binomial theorem is the 44th theorem on Freek Wiedijk’s list of 100 theorems [Wie].

Definitions

Binomial sums

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

Properties

Binomial sums of one and two elements

binomial-sum-one-element-ℕ :
  (f : functional-vec ℕ 1) → binomial-sum-ℕ 0 f ＝ head-functional-vec 0 f
binomial-sum-one-element-ℕ =
  binomial-sum-one-element-Commutative-Semiring ℕ-Commutative-Semiring

binomial-sum-two-elements-ℕ :
  (f : functional-vec ℕ 2) →
  binomial-sum-ℕ 1 f ＝ (f (zero-Fin 1)) +ℕ (f (one-Fin 1))
binomial-sum-two-elements-ℕ =
  binomial-sum-two-elements-Commutative-Semiring ℕ-Commutative-Semiring

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-Semiring ℕ-Commutative-Semiring

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-Semiring ℕ-Commutative-Semiring

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-Semiring
    ℕ-Commutative-Semiring

Theorem

Binomial theorem for the natural numbers

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-Semiring ℕ-Commutative-Semiring

References

[Wie]
Freek Wiedijk. Formalizing 100 theorems. URL: https://www.cs.ru.nl/~freek/100/.

Recent changes