Products of natural numbers
Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.
Created on 2022-02-13.
Last modified on 2023-05-13.
module elementary-number-theory.products-of-natural-numbers where
Imports
open import elementary-number-theory.multiplication-natural-numbers open import elementary-number-theory.natural-numbers open import foundation.coproduct-types open import foundation.unit-type open import lists.lists open import univalent-combinatorics.standard-finite-types
Idea
The product of a list of natural numbers is defined by iterated multiplication.
Definitions
Products of lists of natural numbers
product-list-ℕ : list ℕ → ℕ product-list-ℕ = fold-list 1 mul-ℕ
Products of families of natural numbers indexed by standard finite types
Π-ℕ : (k : ℕ) → (Fin k → ℕ) → ℕ Π-ℕ zero-ℕ x = 1 Π-ℕ (succ-ℕ k) x = (Π-ℕ k (λ i → x (inl i))) *ℕ (x (inr star))
Recent changes
- 2023-05-13. Fredrik Bakke. Refactor to use infix binary operators for arithmetic (#620).
- 2023-04-08. Egbert Rijke. Refactoring elementary number theory files (#546).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497). - 2023-03-07. Fredrik Bakke. Add blank lines between
<details>
tags and markdown syntax (#490). - 2023-03-07. Jonathan Prieto-Cubides. Show module declarations (#488).