Multiplication of the elements of a list of natural numbers

Content created by Fredrik Bakke, Victor Blanchi and Egbert Rijke.

Created on 2023-05-10.
Last modified on 2023-06-10.

module elementary-number-theory.multiplication-lists-of-natural-numbers where
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.action-on-identifications-functions
open import foundation.identity-types

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


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


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


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-ℕ =
    ( 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))

Recent changes