# The binomial theorem for semirings

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

Created on 2023-02-20.

module ring-theory.binomial-theorem-semirings where

Imports
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.binomial-coefficients
open import elementary-number-theory.distance-natural-numbers
open import elementary-number-theory.inequality-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-binary-functions
open import foundation.action-on-identifications-functions
open import foundation.homotopies
open import foundation.identity-types
open import foundation.universe-levels

open import linear-algebra.vectors-on-semirings

open import ring-theory.powers-of-elements-semirings
open import ring-theory.semirings
open import ring-theory.sums-semirings

open import univalent-combinatorics.coproduct-types
open import univalent-combinatorics.standard-finite-types


## Idea

The binomial theorem in semirings asserts that for any two elements x and y of a commutative ring R and any natural number n, if xy = yx holds then we have

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


## Definitions

### Binomial sums

binomial-sum-Semiring :
{l : Level} (R : Semiring l)
(n : ℕ) (f : functional-vec-Semiring R (succ-ℕ n)) →
type-Semiring R
binomial-sum-Semiring R n f =
sum-Semiring R (succ-ℕ n)
( λ i →
mul-nat-scalar-Semiring R
( binomial-coefficient-Fin n i)
( f i))


## Properties

### Binomial sums of one and two elements

module _
{l : Level} (R : Semiring l)
where

binomial-sum-one-element-Semiring :
(f : functional-vec-Semiring R 1) →
binomial-sum-Semiring R 0 f ＝
head-functional-vec-Semiring R 0 f
binomial-sum-one-element-Semiring f =
( sum-one-element-Semiring R
( λ i →
mul-nat-scalar-Semiring R
( binomial-coefficient-Fin 0 i)
( f i))) ∙
( left-unit-law-mul-nat-scalar-Semiring R
( head-functional-vec-Semiring R 0 f))

binomial-sum-two-elements-Semiring :
(f : functional-vec-Semiring R 2) →
binomial-sum-Semiring R 1 f ＝
add-Semiring R (f (zero-Fin 1)) (f (one-Fin 1))
binomial-sum-two-elements-Semiring f =
sum-two-elements-Semiring R
( λ i → mul-nat-scalar-Semiring R (binomial-coefficient-Fin 1 i) (f i)) ∙
( ap-binary
( left-unit-law-mul-nat-scalar-Semiring R (f (zero-Fin 1)))
( left-unit-law-mul-nat-scalar-Semiring R (f (one-Fin 1))))


### Binomial sums are homotopy invariant

module _
{l : Level} (R : Semiring l)
where

htpy-binomial-sum-Semiring :
(n : ℕ) {f g : functional-vec-Semiring R (succ-ℕ n)} →
(f ~ g) →
binomial-sum-Semiring R n f ＝ binomial-sum-Semiring R n g
htpy-binomial-sum-Semiring n H =
htpy-sum-Semiring R
( succ-ℕ n)
( λ i →
ap
( mul-nat-scalar-Semiring R (binomial-coefficient-Fin n i))
( H i))


### Multiplication distributes over sums

module _
{l : Level} (R : Semiring l)
where

left-distributive-mul-binomial-sum-Semiring :
(n : ℕ) (x : type-Semiring R)
(f : functional-vec-Semiring R (succ-ℕ n)) →
mul-Semiring R x (binomial-sum-Semiring R n f) ＝
binomial-sum-Semiring R n (λ i → mul-Semiring R x (f i))
left-distributive-mul-binomial-sum-Semiring n x f =
( left-distributive-mul-sum-Semiring R
( succ-ℕ n)
( x)
( λ i →
mul-nat-scalar-Semiring R (binomial-coefficient-Fin n i) (f i))) ∙
( htpy-sum-Semiring R
( succ-ℕ n)
( λ i →
right-nat-scalar-law-mul-Semiring R
( binomial-coefficient-Fin n i)
( x)
( f i)))

right-distributive-mul-binomial-sum-Semiring :
(n : ℕ) (f : functional-vec-Semiring R (succ-ℕ n)) →
(x : type-Semiring R) →
mul-Semiring R (binomial-sum-Semiring R n f) x ＝
binomial-sum-Semiring R n (λ i → mul-Semiring R (f i) x)
right-distributive-mul-binomial-sum-Semiring n f x =
( right-distributive-mul-sum-Semiring R
( succ-ℕ n)
( λ i →
mul-nat-scalar-Semiring R (binomial-coefficient-Fin n i) (f i))
( x)) ∙
( htpy-sum-Semiring R
( succ-ℕ n)
( λ i →
left-nat-scalar-law-mul-Semiring R
( binomial-coefficient-Fin n i)
( f i)
( x)))


## Lemmas

### Computing a left summand that will appear in the proof of the binomial theorem

module _
{l : Level} (R : Semiring l)
where

left-summand-binomial-theorem-Semiring :
(n : ℕ) (x y : type-Semiring R) →
(H : mul-Semiring R x y ＝ mul-Semiring R y x) →
( mul-Semiring R
( binomial-sum-Semiring R
( succ-ℕ n)
( λ i →
mul-Semiring R
( power-Semiring R (nat-Fin (succ-ℕ (succ-ℕ n)) i) x)
( power-Semiring R
( dist-ℕ (nat-Fin (succ-ℕ (succ-ℕ n)) i) (succ-ℕ n)) y)))
( x)) ＝
( power-Semiring R (succ-ℕ (succ-ℕ n)) x)
( sum-Semiring R
( succ-ℕ n)
( λ i →
mul-nat-scalar-Semiring R
( binomial-coefficient-Fin (succ-ℕ n) (inl-Fin (succ-ℕ n) i))
( mul-Semiring R
( power-Semiring R
( succ-ℕ (nat-Fin (succ-ℕ n) i))
( x))
( power-Semiring R
( dist-ℕ (nat-Fin (succ-ℕ n) i) (succ-ℕ n))
( y))))))
left-summand-binomial-theorem-Semiring n x y H =
( right-distributive-mul-binomial-sum-Semiring R
( succ-ℕ n)
( λ i →
mul-Semiring R
( power-Semiring R
( nat-Fin (succ-ℕ (succ-ℕ n)) i)
( x))
( power-Semiring R
( dist-ℕ (nat-Fin (succ-ℕ (succ-ℕ n)) i) (succ-ℕ n))
( y)))
( x)) ∙
( ( htpy-binomial-sum-Semiring R
( succ-ℕ n)
( λ i →
( ( associative-mul-Semiring R
( power-Semiring R (nat-Fin (succ-ℕ (succ-ℕ n)) i) x)
( power-Semiring R
( dist-ℕ (nat-Fin (succ-ℕ (succ-ℕ n)) i) (succ-ℕ n))
( y))
( x)) ∙
( ( ap
( mul-Semiring R
( power-Semiring R (nat-Fin (succ-ℕ (succ-ℕ n)) i) x))
( commute-powers-Semiring' R
( dist-ℕ (nat-Fin (succ-ℕ (succ-ℕ n)) i) (succ-ℕ n))
( inv H))) ∙
( inv
( associative-mul-Semiring R
( power-Semiring R (nat-Fin (succ-ℕ (succ-ℕ n)) i) x)
( x)
( power-Semiring R
( dist-ℕ (nat-Fin (succ-ℕ (succ-ℕ n)) i) (succ-ℕ n))
( y)))))) ∙
( ap
( mul-Semiring' R
( power-Semiring R
( dist-ℕ (nat-Fin (succ-ℕ (succ-ℕ n)) i) (succ-ℕ n))
( y)))
( inv
( power-succ-Semiring R
( nat-Fin (succ-ℕ (succ-ℕ n)) i)
( x)))))) ∙
( ( ap
( add-Semiring R _)
( ( ap-mul-nat-scalar-Semiring R
( is-one-on-diagonal-binomial-coefficient-ℕ (succ-ℕ n))
( ap
( λ t →
mul-Semiring R
( power-Semiring R (succ-ℕ (succ-ℕ n)) x)
( power-Semiring R t y))
( dist-eq-ℕ' (succ-ℕ n)))) ∙
( ( left-unit-law-mul-nat-scalar-Semiring R
( mul-Semiring R
( power-Semiring R (succ-ℕ (succ-ℕ n)) x)
( one-Semiring R))) ∙
( right-unit-law-mul-Semiring R
( power-Semiring R (succ-ℕ (succ-ℕ n)) x))))) ∙
( sum-Semiring R
( succ-ℕ n)
( λ i →
mul-nat-scalar-Semiring R
( binomial-coefficient-Fin (succ-ℕ n) (inl-Fin (succ-ℕ n) i))
( mul-Semiring R
( power-Semiring R
( succ-ℕ (nat-Fin (succ-ℕ n) i))
( x))
( power-Semiring R
( dist-ℕ (nat-Fin (succ-ℕ n) i) (succ-ℕ n))
( y)))))
( power-Semiring R (succ-ℕ (succ-ℕ n)) x))))


### Computing a right summand that will appear in the proof of the binomial theorem

  right-summand-binomial-theorem-Semiring :
(n : ℕ) (x y : type-Semiring R) →
( mul-Semiring R
( binomial-sum-Semiring R
( succ-ℕ n)
( λ i →
mul-Semiring R
( power-Semiring R
( nat-Fin (succ-ℕ (succ-ℕ n)) i)
( x))
( power-Semiring R
( dist-ℕ (nat-Fin (succ-ℕ (succ-ℕ n)) i) (succ-ℕ n))
( y))))
( y)) ＝
( power-Semiring R (succ-ℕ (succ-ℕ n)) y)
( sum-Semiring R
( succ-ℕ n)
( λ i →
mul-nat-scalar-Semiring R
( binomial-coefficient-ℕ
( succ-ℕ n)
( succ-ℕ (nat-Fin (succ-ℕ (succ-ℕ n)) (inl-Fin (succ-ℕ n) i))))
( mul-Semiring R
( power-Semiring R
( succ-ℕ (nat-Fin (succ-ℕ n) i))
( x))
( power-Semiring R
( dist-ℕ (nat-Fin (succ-ℕ n) i) (succ-ℕ n))
( y))))))
right-summand-binomial-theorem-Semiring n x y =
( right-distributive-mul-binomial-sum-Semiring R
( succ-ℕ n)
( λ i →
mul-Semiring R
( power-Semiring R
( nat-Fin (succ-ℕ (succ-ℕ n)) i)
( x))
( power-Semiring R
( dist-ℕ (nat-Fin (succ-ℕ (succ-ℕ n)) i) (succ-ℕ n))
( y)))
( y)) ∙
( ( htpy-binomial-sum-Semiring R
( succ-ℕ n)
( λ i →
( associative-mul-Semiring R
( power-Semiring R
( nat-Fin (succ-ℕ (succ-ℕ n)) i)
( x))
( power-Semiring R
( dist-ℕ (nat-Fin (succ-ℕ (succ-ℕ n)) i) (succ-ℕ n))
( y))
( y)) ∙
( ap
( mul-Semiring R
( power-Semiring R
( nat-Fin (succ-ℕ (succ-ℕ n)) i)
( x)))
( inv
( ap
( λ m → power-Semiring R m y)
( right-successor-law-dist-ℕ
( nat-Fin (succ-ℕ (succ-ℕ n)) i)
( succ-ℕ n)
( upper-bound-nat-Fin (succ-ℕ n) i)) ∙
( power-succ-Semiring R
( dist-ℕ (nat-Fin (succ-ℕ (succ-ℕ n)) i) (succ-ℕ n))
( y))))))) ∙
( ( snoc-sum-Semiring R
( succ-ℕ n)
( λ i →
mul-nat-scalar-Semiring R
( binomial-coefficient-Fin (succ-ℕ n) i)
( mul-Semiring R
( power-Semiring R
( nat-Fin (succ-ℕ (succ-ℕ n)) i)
( x))
( power-Semiring R
( dist-ℕ (nat-Fin (succ-ℕ (succ-ℕ n)) i) (succ-ℕ (succ-ℕ n)))
( y))))
( ( ap
( λ m →
mul-nat-scalar-Semiring R
( binomial-coefficient-ℕ (succ-ℕ n) m)
( mul-Semiring R
( power-Semiring R m x)
( power-Semiring R
( dist-ℕ m (succ-ℕ (succ-ℕ n)))
( y))))
( is-zero-nat-zero-Fin {n})) ∙
( ( left-unit-law-mul-nat-scalar-Semiring R
( mul-Semiring R
( one-Semiring R)
( power-Semiring R (succ-ℕ (succ-ℕ n)) y))) ∙
( left-unit-law-mul-Semiring R
( power-Semiring R (succ-ℕ (succ-ℕ n)) y))))) ∙
( refl)
( htpy-sum-Semiring R
( succ-ℕ n)
( λ i →
( ap
( λ m →
mul-nat-scalar-Semiring R
( binomial-coefficient-ℕ (succ-ℕ n) m)
( mul-Semiring R
( power-Semiring R m x)
( power-Semiring R
( dist-ℕ m (succ-ℕ (succ-ℕ n)))
( y))))
( nat-inr-Fin (succ-ℕ n) i)))))))


## Theorem

### Binomial theorem for semirings

binomial-theorem-Semiring :
{l : Level} (R : Semiring l) (n : ℕ) (x y : type-Semiring R) →
mul-Semiring R x y ＝ mul-Semiring R y x →
power-Semiring R n (add-Semiring R x y) ＝
binomial-sum-Semiring R n
( λ i →
mul-Semiring R
( power-Semiring R (nat-Fin (succ-ℕ n) i) x)
( power-Semiring R (dist-ℕ (nat-Fin (succ-ℕ n) i) n) y))
binomial-theorem-Semiring R zero-ℕ x y H =
inv
( ( sum-one-element-Semiring R
( λ i →
mul-nat-scalar-Semiring R
( binomial-coefficient-Fin 0 i)
( mul-Semiring R
( power-Semiring R (nat-Fin 1 i) x)
( power-Semiring R (dist-ℕ (nat-Fin 1 i) 0) y)))) ∙
( ( left-unit-law-mul-nat-scalar-Semiring R
( mul-Semiring R
( one-Semiring R)
( one-Semiring R))) ∙
( left-unit-law-mul-Semiring R (one-Semiring R))))
binomial-theorem-Semiring R (succ-ℕ zero-ℕ) x y H =
( commutative-add-Semiring R x y) ∙
( ( ap-binary
( ( inv (left-unit-law-mul-Semiring R y)) ∙
( inv
( left-unit-law-mul-nat-scalar-Semiring R
( mul-Semiring R (one-Semiring R) y))))
( ( inv (right-unit-law-mul-Semiring R x)) ∙
( inv
( left-unit-law-mul-nat-scalar-Semiring R
( mul-Semiring R x (one-Semiring R)))))) ∙
( inv
( sum-two-elements-Semiring R
( λ i →
mul-nat-scalar-Semiring R
( binomial-coefficient-Fin 1 i)
( mul-Semiring R
( power-Semiring R (nat-Fin 2 i) x)
( power-Semiring R (dist-ℕ (nat-Fin 2 i) 1) y))))))
binomial-theorem-Semiring R (succ-ℕ (succ-ℕ n)) x y H =
( ap
( λ r → mul-Semiring R r (add-Semiring R x y))
( binomial-theorem-Semiring R (succ-ℕ n) x y H)) ∙
( ( left-distributive-mul-add-Semiring R _ x y) ∙
( ( ap-add-Semiring R
( left-summand-binomial-theorem-Semiring R n x y H)
( right-summand-binomial-theorem-Semiring R n x y)) ∙
( power-Semiring R (succ-ℕ (succ-ℕ n)) x)
( sum-Semiring R
( succ-ℕ n)
( λ i →
mul-nat-scalar-Semiring R
( binomial-coefficient-Fin (succ-ℕ n) (inl-Fin (succ-ℕ n) i))
( mul-Semiring R
( power-Semiring R
( succ-ℕ (nat-Fin (succ-ℕ n) i))
( x))
( power-Semiring R
( dist-ℕ (nat-Fin (succ-ℕ n) i) (succ-ℕ n))
( y)))))
( power-Semiring R (succ-ℕ (succ-ℕ n)) y)
( sum-Semiring R
( succ-ℕ n)
( λ i →
mul-nat-scalar-Semiring R
( binomial-coefficient-ℕ
( succ-ℕ n)
( succ-ℕ (nat-Fin (succ-ℕ (succ-ℕ n)) (inl-Fin (succ-ℕ n) i))))
( mul-Semiring R
( power-Semiring R
( succ-ℕ (nat-Fin (succ-ℕ n) i))
( x))
( power-Semiring R
( dist-ℕ (nat-Fin (succ-ℕ n) i) (succ-ℕ n))
( y)))))) ∙
( ( ap-add-Semiring R
( power-Semiring R (succ-ℕ (succ-ℕ n)) x)
( power-Semiring R (succ-ℕ (succ-ℕ n)) y))
( ( interchange-add-sum-Semiring R
( succ-ℕ n)
( λ i →
mul-nat-scalar-Semiring R
( binomial-coefficient-Fin (succ-ℕ n) (inl-Fin (succ-ℕ n) i))
( mul-Semiring R
( power-Semiring R
( succ-ℕ (nat-Fin (succ-ℕ n) i))
( x))
( power-Semiring R
( dist-ℕ (nat-Fin (succ-ℕ n) i) (succ-ℕ n))
( y))))
( λ i →
mul-nat-scalar-Semiring R
( binomial-coefficient-ℕ
( succ-ℕ n)
( succ-ℕ
( nat-Fin (succ-ℕ (succ-ℕ n)) (inl-Fin (succ-ℕ n) i))))
( mul-Semiring R
( power-Semiring R
( succ-ℕ (nat-Fin (succ-ℕ n) i))
( x))
( power-Semiring R
( dist-ℕ (nat-Fin (succ-ℕ n) i) (succ-ℕ n))
( y))))) ∙
( htpy-sum-Semiring R
( succ-ℕ n)
( λ i →
( inv
( binomial-coefficient-ℕ
( succ-ℕ n)
( nat-Fin (succ-ℕ n) i))
( binomial-coefficient-ℕ
( succ-ℕ n)
( succ-ℕ (nat-Fin (succ-ℕ n) i)))
( mul-Semiring R
( power-Semiring R
( succ-ℕ (nat-Fin (succ-ℕ n) i))
( x))
( power-Semiring R
( dist-ℕ (nat-Fin (succ-ℕ n) i) (succ-ℕ n))
( y))))) ∙
( ap
( λ m →
mul-nat-scalar-Semiring R
( binomial-coefficient-ℕ (succ-ℕ (succ-ℕ n)) m)
( mul-Semiring R
( power-Semiring R m x)
( power-Semiring R
( dist-ℕ m (succ-ℕ (succ-ℕ n)))
( y))))
( inv (nat-inr-Fin (succ-ℕ n) i))))))) ∙
( ( right-swap-add-Semiring R
( power-Semiring R (succ-ℕ (succ-ℕ n)) y)
( power-Semiring R (succ-ℕ (succ-ℕ n)) x)
( _)) ∙
( ( ap
( power-Semiring R (succ-ℕ (succ-ℕ n)) x))
( inv
( snoc-sum-Semiring R
( succ-ℕ n)
( λ i →
mul-nat-scalar-Semiring R
( binomial-coefficient-ℕ
( succ-ℕ (succ-ℕ n))
( nat-Fin (succ-ℕ (succ-ℕ n)) i))
( mul-Semiring R
( power-Semiring R
( nat-Fin (succ-ℕ (succ-ℕ n)) i)
( x))
( power-Semiring R
( dist-ℕ
( nat-Fin (succ-ℕ (succ-ℕ n)) i)
( succ-ℕ (succ-ℕ n)))
( y))))
( ( ap
( λ m →
mul-nat-scalar-Semiring R
( binomial-coefficient-ℕ (succ-ℕ (succ-ℕ n)) m)
( mul-Semiring R
( power-Semiring R m x)
( power-Semiring R
( dist-ℕ m (succ-ℕ (succ-ℕ n)))
( y))))
( is-zero-nat-zero-Fin {n})) ∙
( ( left-unit-law-mul-nat-scalar-Semiring R
( mul-Semiring R
( one-Semiring R)
( power-Semiring R
( succ-ℕ (succ-ℕ n))
( y)))) ∙
( left-unit-law-mul-Semiring R
( power-Semiring R
( succ-ℕ (succ-ℕ n))
( y)))))))) ∙
( inv
( cons-sum-Semiring R
( succ-ℕ (succ-ℕ n))
( λ i →
mul-nat-scalar-Semiring R
( binomial-coefficient-Fin (succ-ℕ (succ-ℕ n)) i)
( mul-Semiring R
( power-Semiring R
( nat-Fin (succ-ℕ (succ-ℕ (succ-ℕ n))) i)
( x))
( power-Semiring R
( dist-ℕ
( nat-Fin (succ-ℕ (succ-ℕ (succ-ℕ n))) i)
( succ-ℕ (succ-ℕ n)))
( y))))
( ( ap-mul-nat-scalar-Semiring R
( is-one-on-diagonal-binomial-coefficient-ℕ
( succ-ℕ (succ-ℕ n)))
( ( ap
( mul-Semiring R
( power-Semiring R (succ-ℕ (succ-ℕ n)) x))
( ap
( λ m → power-Semiring R m y)
( dist-eq-ℕ' (succ-ℕ (succ-ℕ n))))) ∙
( right-unit-law-mul-Semiring R
( power-Semiring R (succ-ℕ (succ-ℕ n)) x)))) ∙
( left-unit-law-mul-nat-scalar-Semiring R
( power-Semiring R
( succ-ℕ (succ-ℕ n))
( x))))))))))))


## Corollaries

### If x commutes with y, then we can compute (x+y)ⁿ⁺ᵐ as a linear combination of xⁿ and yᵐ

is-linear-combination-power-add-Semiring :
{l : Level} (R : Semiring l) (n m : ℕ) (x y : type-Semiring R) →
mul-Semiring R x y ＝ mul-Semiring R y x →
power-Semiring R (n +ℕ m) (add-Semiring R x y) ＝
( mul-Semiring R
( power-Semiring R m y)
( sum-Semiring R n
( λ i →
mul-nat-scalar-Semiring R
( binomial-coefficient-ℕ (n +ℕ m) (nat-Fin n i))
( mul-Semiring R
( power-Semiring R (nat-Fin n i) x)
( power-Semiring R (dist-ℕ (nat-Fin n i) n) y)))))
( mul-Semiring R
( power-Semiring R n x)
( sum-Semiring R
( succ-ℕ m)
( λ i →
mul-nat-scalar-Semiring R
( binomial-coefficient-ℕ
( n +ℕ m)
( n +ℕ (nat-Fin (succ-ℕ m) i)))
( mul-Semiring R
( power-Semiring R (nat-Fin (succ-ℕ m) i) x)
( power-Semiring R (dist-ℕ (nat-Fin (succ-ℕ m) i) m) y)))))
is-linear-combination-power-add-Semiring R n m x y H =
( binomial-theorem-Semiring R (n +ℕ m) x y H) ∙
( ( split-sum-Semiring R n
( succ-ℕ m)
( λ i →
mul-nat-scalar-Semiring R
( binomial-coefficient-ℕ
( n +ℕ m)
( nat-Fin (n +ℕ (succ-ℕ m)) i))
( mul-Semiring R
( power-Semiring R
( nat-Fin (n +ℕ (succ-ℕ m)) i)
( x))
( power-Semiring R
( dist-ℕ
( nat-Fin (n +ℕ (succ-ℕ m)) i)
( n +ℕ m))
( y))))) ∙
( ( ap-add-Semiring R
( ( htpy-sum-Semiring R n
( λ i →
( ap
( λ u →
mul-nat-scalar-Semiring R
( binomial-coefficient-ℕ (n +ℕ m) u)
( mul-Semiring R
( power-Semiring R u x)
( power-Semiring R
( dist-ℕ u (n +ℕ m))
( y))))
( nat-inl-coproduct-Fin n m i)) ∙
( ( ( ap
( mul-nat-scalar-Semiring R
( binomial-coefficient-ℕ
( n +ℕ m)
( nat-Fin n i)))
( ( ap
( mul-Semiring R
( power-Semiring R
( nat-Fin n i)
( x)))
( ( ap
( λ u → power-Semiring R u y)
( ( inv
( triangle-equality-dist-ℕ
( nat-Fin n i)
( n)
( n +ℕ m)
( upper-bound-nat-Fin' n i)
( leq-add-ℕ n m)) ∙
( ap
( (dist-ℕ (nat-Fin n i) n) +ℕ_)
( dist-add-ℕ n m))) ∙
( dist-ℕ (nat-Fin n i) n)
( m)))) ∙
( ( distributive-power-add-Semiring R m
( dist-ℕ (nat-Fin n i) n))))) ∙
( ( inv
( associative-mul-Semiring R
( power-Semiring R (nat-Fin n i) x)
( power-Semiring R m y)
( power-Semiring R (dist-ℕ (nat-Fin n i) n) y))) ∙
( ( ap
( mul-Semiring' R
( power-Semiring R (dist-ℕ (nat-Fin n i) n) y))
( commute-powers-Semiring R (nat-Fin n i) m H)) ∙
( associative-mul-Semiring R
( power-Semiring R m y)
( power-Semiring R (nat-Fin n i) x)
( power-Semiring R
( dist-ℕ (nat-Fin n i) n)
( y))))))) ∙
( inv
( right-nat-scalar-law-mul-Semiring R
( binomial-coefficient-ℕ
( n +ℕ m)
( nat-Fin n i))
( power-Semiring R m y)
( mul-Semiring R
( power-Semiring R (nat-Fin n i) x)
( power-Semiring R
( dist-ℕ (nat-Fin n i) n)
( y))))))))) ∙
( ( inv
( left-distributive-mul-sum-Semiring R n
( power-Semiring R m y)
( λ i →
mul-nat-scalar-Semiring R
( binomial-coefficient-ℕ (n +ℕ m) (nat-Fin n i))
( mul-Semiring R
( power-Semiring R (nat-Fin n i) x)
( power-Semiring R (dist-ℕ (nat-Fin n i) n) y)))))))
( ( htpy-sum-Semiring R
( succ-ℕ m)
( λ i →
( ap
( λ u →
mul-nat-scalar-Semiring R
( binomial-coefficient-ℕ (n +ℕ m) u)
( mul-Semiring R
( power-Semiring R u x)
( power-Semiring R
( dist-ℕ u (n +ℕ m))
( y))))
( nat-inr-coproduct-Fin n (succ-ℕ m) i)) ∙
( ( ap
( mul-nat-scalar-Semiring R
( binomial-coefficient-ℕ
( n +ℕ m)
( n +ℕ (nat-Fin (succ-ℕ m) i))))
( ap-mul-Semiring R
( distributive-power-add-Semiring R n
( nat-Fin (succ-ℕ m) i))
( ap
( λ u → power-Semiring R u y)
( translation-invariant-dist-ℕ
( n)
( nat-Fin (succ-ℕ m) i)
( m))) ∙
( associative-mul-Semiring R
( power-Semiring R n x)
( power-Semiring R (nat-Fin (succ-ℕ m) i) x)
( power-Semiring R
( dist-ℕ (nat-Fin (succ-ℕ m) i) m)
( y))))) ∙
( inv
( right-nat-scalar-law-mul-Semiring R
( binomial-coefficient-ℕ
( n +ℕ m)
( n +ℕ (nat-Fin (succ-ℕ m) i)))
( power-Semiring R n x)
( mul-Semiring R
( power-Semiring R (nat-Fin (succ-ℕ m) i) x)
( power-Semiring R
( dist-ℕ (nat-Fin (succ-ℕ m) i) m)
( y)))))))) ∙
( inv
( left-distributive-mul-sum-Semiring R
( succ-ℕ m)
( power-Semiring R n x)
( λ i →
mul-nat-scalar-Semiring R
( binomial-coefficient-ℕ
( n +ℕ m)
( n +ℕ (nat-Fin (succ-ℕ m) i)))
( mul-Semiring R
( power-Semiring R (nat-Fin (succ-ℕ m) i) x)
( power-Semiring R
( dist-ℕ (nat-Fin (succ-ℕ m) i) m)
( y))))))))))