# Multiples of elements in commutative rings

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-09-10.

module commutative-algebra.multiples-of-elements-commutative-rings where

Imports
open import commutative-algebra.commutative-rings

open import elementary-number-theory.multiplication-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.identity-types
open import foundation.universe-levels

open import ring-theory.multiples-of-elements-rings


## Idea

For any commutative ring A there is a multiplication operation ℕ → A → A, which we write informally as n x ↦ n · x. This operation is defined by iteratively adding x with itself n times.

## Definition

### Natural number multiples of elements of commutative rings

module _
{l : Level} (A : Commutative-Ring l)
where

multiple-Commutative-Ring :
ℕ → type-Commutative-Ring A → type-Commutative-Ring A
multiple-Commutative-Ring =
multiple-Ring (ring-Commutative-Ring A)


## Properties

### n · 0 ＝ 0

module _
{l : Level} (A : Commutative-Ring l)
where

multiple-zero-Commutative-Ring :
(n : ℕ) →
multiple-Commutative-Ring A n (zero-Commutative-Ring A) ＝
zero-Commutative-Ring A
multiple-zero-Commutative-Ring =
multiple-zero-Ring (ring-Commutative-Ring A)


### (n + 1) · x = n · x + x

module _
{l : Level} (A : Commutative-Ring l)
where

multiple-succ-Commutative-Ring :
(n : ℕ) (x : type-Commutative-Ring A) →
multiple-Commutative-Ring A (succ-ℕ n) x ＝
add-Commutative-Ring A (multiple-Commutative-Ring A n x) x
multiple-succ-Commutative-Ring =
multiple-succ-Ring (ring-Commutative-Ring A)


### (n + 1) · x ＝ x + n · x

module _
{l : Level} (A : Commutative-Ring l)
where

multiple-succ-Commutative-Ring' :
(n : ℕ) (x : type-Commutative-Ring A) →
multiple-Commutative-Ring A (succ-ℕ n) x ＝
add-Commutative-Ring A x (multiple-Commutative-Ring A n x)
multiple-succ-Commutative-Ring' =
multiple-succ-Ring' (ring-Commutative-Ring A)


### Multiples by sums of natural numbers are products of multiples

module _
{l : Level} (A : Commutative-Ring l)
where

(m n : ℕ) {x : type-Commutative-Ring A} →
multiple-Commutative-Ring A (m +ℕ n) x ＝
( multiple-Commutative-Ring A m x)
( multiple-Commutative-Ring A n x)


### Multiples distribute over the sum of x and y

module _
{l : Level} (A : Commutative-Ring l)
where

(n : ℕ) {x y : type-Commutative-Ring A} →
multiple-Commutative-Ring A n (add-Commutative-Ring A x y) ＝
( multiple-Commutative-Ring A n x)
( multiple-Commutative-Ring A n y)


### Multiples by products of natural numbers are iterated multiples

module _
{l : Level} (A : Commutative-Ring l)
where

multiple-mul-Commutative-Ring :
(m n : ℕ) {x : type-Commutative-Ring A} →
multiple-Commutative-Ring A (m *ℕ n) x ＝
multiple-Commutative-Ring A n (multiple-Commutative-Ring A m x)
multiple-mul-Commutative-Ring =
multiple-mul-Ring (ring-Commutative-Ring A)