Multiplication of the elements of a list of natural numbers

module elementary-number-theory.multiplication-lists-of-natural-numbers where
Imports
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.multiplication-natural-numbers
open import elementary-number-theory.natural-numbers

open import finite-group-theory.permutations-standard-finite-types

open import foundation.identity-types

open import lists.concatenation-lists
open import lists.lists
open import lists.permutation-lists

Idea

Given a list of natural number l, we define the product of the element of the list.

Definition

mul-list-ℕ :
  list   
mul-list-ℕ = fold-list 1 mul-ℕ

Properties

mul-list-ℕ is invariant by permutation

invariant-permutation-mul-list-ℕ :
  (l : list ) (t : Permutation (length-list l)) 
  mul-list-ℕ l  mul-list-ℕ (permute-list l t)
invariant-permutation-mul-list-ℕ =
  invariant-permutation-fold-list
    ( 1)
    ( mul-ℕ)
    ( λ a1 a2 b 
      ( inv (associative-mul-ℕ a1 a2 b) 
        ( ap  n  n *ℕ b) (commutative-mul-ℕ a1 a2) 
          ( associative-mul-ℕ a2 a1 b))))

mul-list-ℕ of a concatenation of lists

eq-mul-list-concat-list-ℕ :
  (p q : list ) 
  (mul-list-ℕ (concat-list p q))  (mul-list-ℕ p) *ℕ (mul-list-ℕ q)
eq-mul-list-concat-list-ℕ nil q = inv (left-unit-law-add-ℕ (mul-list-ℕ q))
eq-mul-list-concat-list-ℕ (cons x p) q =
  ap (mul-ℕ x) (eq-mul-list-concat-list-ℕ p q) 
  inv (associative-mul-ℕ x (mul-list-ℕ p) (mul-list-ℕ q))