Contents

Contents

Idea

The inverse operation to multiplication.

Definition

In an Euclidean domain

See Euclidean domain

In a field

Given a Heyting field $F$, let us define the type of all terms in $F$ apart from 0:

$F_{#0} \coloneqq \{a \in F \vert a # 0\}$

The division function is a binary function $\frac{(-)}{(-)}:F \times F_{#0} \to F$ defined as

$\frac{x}{y} \coloneqq x \cdot \frac{1}{y}$

where

$\frac{1}{y}$

is the reciprocal function.

Division of finite sets

Given finite set $A$ and pointed set $B$ with an element $p:B$, one can construct finite sets $A \div B$ and $A\ \%\ B$ with a bijection

$A \simeq ((B \times (A \div B)) + (A\ \%\ B))$

and a bijection

$(B \hookrightarrow A\ \%\ B) \simeq \emptyset$

A finite pointed set $B$ is a divisor of $A$ if there is a bijection $(A\ \%\ B) \simeq \emptyset$:

$A \vert B \coloneqq (A\ \%\ B) \simeq \emptyset$

Last revised on February 27, 2024 at 06:30:33. See the history of this page for a list of all contributions to it.