Definitions: Mathlib.Data, part 3 of 6

AddEquiv.mapMatrixdefMathlib.Data.Matrix.Basic, function or constant

Wording

the map matrix of f (from the name)

English

Let $f$ be an additive equivalence of $x$ and $x_{1}$. Then the map matrix of $f$ is an additive equivalence of the set of matrixes of $n$ and $x$ and the set of matrixes of $n$ and $x_{1}$.

AddMonoidHom.mapMatrixdefMathlib.Data.Matrix.Basic, function or constant

Wording

the map matrix of f (from the name)

English

Let $f$ be an additive monoid homomorphism of $x$ and $x_{1}$. Then the map matrix of $f$ is an additive monoid homomorphism of the set of matrixes of $n$ and $x$ and the set of matrixes of $n$ and $x_{1}$.

AddSubgroup.matrixdefMathlib.Data.Matrix.Basic, function or constant

Wording

the matrix of S (from the name)

English

Let $S$ be an additive subgroup of $A$. Then the matrix of $S$ is an additive subgroup of the set of matrixes of $n$ and $A$.

AddSubmonoid.matrixdefMathlib.Data.Matrix.Basic, function or constant

Wording

the matrix of S (from the name)

English

Let $S$ be an additive submonoid of $A$. Then the matrix of $S$ is an additive submonoid of the set of matrixes of $n$ and $A$.

AlgEquiv.mapMatrixdefMathlib.Data.Matrix.Basic, function or constant

Wording

the map matrix of f (from the name)

English

Let $f$ be an algebra isomorphism of $x$ and $x_{1}$. Then the map matrix of $f$ is an algebra isomorphism of the set of matrixes of $m$ and $x$ and the set of matrixes of $m$ and $x_{1}$.

AlgEquiv.mopMatrixdefMathlib.Data.Matrix.Basic, function or constant

Wording

no wording

English

$\operatorname{mopMatrix}$ is an algebra isomorphism of the set of matrixes of $m$ and the set of multiplicative opposites of $x$ and the set of multiplicative opposites of the set of matrixes of $m$ and $x$.

AlgHom.mapMatrixdefMathlib.Data.Matrix.Basic, function or constant

Wording

the map matrix of f (from the name)

English

Let $f$ be an algebra homomorphism of $x$ and $x_{1}$. Then the map matrix of $f$ is an algebra homomorphism of the set of matrixes of $m$ and $x$ and the set of matrixes of $m$ and $x_{1}$.

Equiv.mapMatrixdefMathlib.Data.Matrix.Basic, function or constant

Wording

the map matrix of f (from the name)

English

Let $f$ be an equivalence from $x$ to $x_{1}$. Then the map matrix of $f$ is an equivalence from the set of matrixes of $n$ and $x$ to the set of matrixes of $n$ and $x_{1}$.

LinearEquiv.mapMatrixdefMathlib.Data.Matrix.Basic, function or constant

Wording

the map matrix of f (from the name)

English

Let $f$ be a linear equivalence of $x$ and $x_{1}$. Then the map matrix of $f$ is a linear equivalence of the set of matrixes of $n$ and $x$ and the set of matrixes of $n$ and $x_{1}$.

LinearMap.mapMatrixdefMathlib.Data.Matrix.Basic, function or constant

Wording

the map matrix of f (from the name)

English

Let $f$ be a linear map of $x$ and $x_{1}$. Then the map matrix of $f$ is a linear map of the set of matrixes of $n$ and $x$ and the set of matrixes of $n$ and $x_{1}$.

LinearMap.mapMatrixLineardefMathlib.Data.Matrix.Basic, function or constant

Wording

no wording

English

Let $A$ be a set. Then $\operatorname{mapMatrixLinear}$ applied to $A$ is a linear map of the set of linear maps of $x$ and $x_{1}$ and the set of linear maps of the set of matrixes of $n$ and $x$ and the set of matrixes of $n$ and $x_{1}$.

Matrix.diagAddMonoidHomdefMathlib.Data.Matrix.Basic, function or constant

Wording

the diagonal additive monoid homomorphism of n and x (from the name)

English

Let $n$ and $x$ be sets. Then the diagonal additive monoid homomorphism of $n$ and $x$ is an additive monoid homomorphism of the set of matrixes of $n$ and $x$ and the set of functions from elements of $n$ to elements of $x$.

Matrix.diagLinearMapdefMathlib.Data.Matrix.Basic, function or constant

Wording

the diagonal linear map of R and x (from the name)

English

Let $n$, $R$ and $x$ be sets. Then the diagonal linear map of $R$ and $x$ is a linear map of the set of matrixes of $n$ and $x$ and the set of functions from elements of $n$ to elements of $x$.

Matrix.diagonalAddMonoidHomdefMathlib.Data.Matrix.Basic, function or constant

Wording

the diagonal additive monoid homomorphism of n and x (from the name)

English

Let $n$ and $x$ be sets. Then the diagonal additive monoid homomorphism of $n$ and $x$ is an additive monoid homomorphism of the set of functions from elements of $n$ to elements of $x$ and the set of matrixes of $n$ and $x$.

Matrix.diagonalAlgHomdefMathlib.Data.Matrix.Basic, function or constant

Wording

the diagonal algebra homomorphism of R (from the name)

English

Let $R$ be a set. Then the diagonal algebra homomorphism of $R$ is an algebra homomorphism of the set of functions from elements of $n$ to elements of $x$ and the set of matrixes of $n$ and $x$.

Matrix.diagonalLinearMapdefMathlib.Data.Matrix.Basic, function or constant

Wording

the diagonal linear map of R and x (from the name)

English

Let $n$, $R$ and $x$ be sets. Then the diagonal linear map of $R$ and $x$ is a linear map of the set of functions from elements of $n$ to elements of $x$ and the set of matrixes of $n$ and $x$.

Matrix.diagonalRingHomdefMathlib.Data.Matrix.Basic, function or constant

Wording

the diagonal ring homomorphism of n and x (from the name)

English

Let $n$ and $x$ be sets. Then the diagonal ring homomorphism of $n$ and $x$ is a ring homomorphism of the set of functions from elements of $n$ to elements of $x$ and the set of matrixes of $n$ and $x$.

Matrix.entryAddHomdefMathlib.Data.Matrix.Basic, function or constant

Wording

the entry additive homomorphism of i and j (from the name)

English

Let $x$ be a set. Let $i$ be an element of $m$. Let $j$ be an element of $n$. Then the entry additive homomorphism of $i$ and $j$ is an additive homomorphism of the set of matrixes of $n$ and $x$ and $x$.

Matrix.entryAddMonoidHomdefMathlib.Data.Matrix.Basic, function or constant

Wording

the entry additive monoid homomorphism of i and j (from the name)

English

Let $x$ be a set. Let $i$ be an element of $m$. Let $j$ be an element of $n$. Then the entry additive monoid homomorphism of $i$ and $j$ is an additive monoid homomorphism of the set of matrixes of $n$ and $x$ and $x$.

Matrix.entryLinearMapdefMathlib.Data.Matrix.Basic, function or constant

Wording

the entry linear map of i and j (from the name)

English

Let $R$ and $x$ be sets. Let $i$ be an element of $m$. Let $j$ be an element of $n$. Then the entry linear map of $i$ and $j$ is a linear map of the set of matrixes of $n$ and $x$ and $x$.

Matrix.ofLinearEquivdefMathlib.Data.Matrix.Basic, function or constant

Wording

the matrix of R (from the name)

English

Let $R$ be a set. Then the matrix of $R$ is a linear equivalence of the set of functions from elements of $m$ and elements of $n$ to elements of $x$ and the set of matrixes of $n$ and $x$.

Matrix.piAddEquivdefMathlib.Data.Matrix.Basic, function or constant

Wording

the product additive equivalence (from the name)

English

The product additive equivalence is an additive equivalence of the set of matrixes of $n$ and the set of functions from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$ and the set of functions from elements $i_{1}$ of $x$ to matrixes of $n$ and $x_{1}$ applied to $i_{1}$.

Matrix.piAlgEquivdefMathlib.Data.Matrix.Basic, function or constant

Wording

the product algebra isomorphism of R (from the name)

English

Let $R$ be a set. Then the product algebra isomorphism of $R$ is an algebra isomorphism of the set of matrixes of $n$ and the set of functions from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$ and the set of functions from elements $i_{1}$ of $x$ to matrixes of $n$ and $x_{1}$ applied to $i_{1}$.

Matrix.piEquivdefMathlib.Data.Matrix.Basic, function or constant

Wording

the product equivalence (from the name)

English

The product equivalence is an equivalence from the set of matrixes of $n$ and the set of functions from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$ to the set of functions from elements $i_{1}$ of $x$ to matrixes of $n$ and $x_{1}$ applied to $i_{1}$.

Matrix.piLinearEquivdefMathlib.Data.Matrix.Basic, function or constant

Wording

the product linear equivalence of R (from the name)

English

Let $R$ be a set. Then the product linear equivalence of $R$ is a linear equivalence of the set of matrixes of $n$ and the set of functions from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$ and the set of functions from elements $i_{1}$ of $x$ to matrixes of $n$ and $x_{1}$ applied to $i_{1}$.

Matrix.piRingEquivdefMathlib.Data.Matrix.Basic, function or constant

Wording

the product ring isomorphism (from the name)

English

The product ring isomorphism is a ring isomorphism of the set of matrixes of $n$ and the set of functions from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$ and the set of functions from elements $i_{1}$ of $x$ to matrixes of $n$ and $x_{1}$ applied to $i_{1}$.

Matrix.scalardefMathlib.Data.Matrix.Basic, function or constant

Wording

the scalar of n (from the name)

English

Let $n$ be a set. Then the scalar of $n$ is a ring homomorphism of $x$ and the set of matrixes of $n$ and $x$ defined as the composition of the diagonal ring homomorphism of $n$ and $x$ and the constant ring homomorphism of $n$ and $x$.

Matrix.scalarAlgHomdefMathlib.Data.Matrix.Basic, function or constant

Wording

the scalar algebra homomorphism of n and R (from the name)

English

Let $n$ and $R$ be sets. Then the scalar algebra homomorphism of $n$ and $R$ is an algebra homomorphism of $x$ and the set of matrixes of $n$ and $x$.

Matrix.transposeAddEquivdefMathlib.Data.Matrix.Basic, function or constant

Wording

the transpose additive equivalence of n and x (from the name)

English

Let $m$, $n$ and $x$ be sets. Then the transpose additive equivalence of $n$ and $x$ is an additive equivalence of the set of matrixes of $n$ and $x$ and the set of matrixes of $m$ and $x$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{transpose}$, $\operatorname{transpose}$, $\mathrm{Matrix\_\_transpose\_transpose}$ and $\mathrm{Matrix\_\_transpose\_transpose}$ and $\mathrm{Matrix\_\_transpose\_add}$.

Matrix.transposeAlgEquivdefMathlib.Data.Matrix.Basic, function or constant

Wording

the transpose algebra isomorphism of R and x (from the name)

English

Let $m$, $R$ and $x$ be sets. Then the transpose algebra isomorphism of $R$ and $x$ is an algebra isomorphism of the set of matrixes of $m$ and $x$ and the set of multiplicative opposites of the set of matrixes of $m$ and $x$.

Matrix.transposeLinearEquivdefMathlib.Data.Matrix.Basic, function or constant

Wording

the transpose linear equivalence of R and x (from the name)

English

Let $m$, $n$, $R$ and $x$ be sets. Then the transpose linear equivalence of $R$ and $x$ is a linear equivalence of the set of matrixes of $n$ and $x$ and the set of matrixes of $m$ and $x$.

Matrix.transposeRingEquivdefMathlib.Data.Matrix.Basic, function or constant

Wording

the transpose ring isomorphism of m and x (from the name)

English

Let $m$ and $x$ be sets. Then the transpose ring isomorphism of $m$ and $x$ is a ring isomorphism of the set of matrixes of $m$ and $x$ and the set of multiplicative opposites of the set of matrixes of $m$ and $x$.

RingEquiv.mapMatrixdefMathlib.Data.Matrix.Basic, function or constant

Wording

the map matrix of f (from the name)

English

Let $f$ be a ring isomorphism of $x$ and $x_{1}$. Then the map matrix of $f$ is a ring isomorphism of the set of matrixes of $m$ and $x$ and the set of matrixes of $m$ and $x_{1}$.

RingEquiv.mopMatrixdefMathlib.Data.Matrix.Basic, function or constant

Wording

no wording

English

$\operatorname{mopMatrix}$ is a ring isomorphism of the set of matrixes of $m$ and the set of multiplicative opposites of $x_{1}$ and the set of multiplicative opposites of the set of matrixes of $m$ and $x_{1}$.

RingHom.mapMatrixdefMathlib.Data.Matrix.Basic, function or constant

Wording

the map matrix of f (from the name)

English

Let $f$ be a ring homomorphism of $x$ and $x_{1}$. Then the map matrix of $f$ is a ring homomorphism of the set of matrixes of $m$ and $x$ and the set of matrixes of $m$ and $x_{1}$.

Submodule.matrixdefMathlib.Data.Matrix.Basic, function or constant

Wording

the matrix of S (from the name)

English

Let $S$ be a submodule of $R$ and $M$. Then the matrix of $S$ is a submodule of $R$ and the set of matrixes of $n$ and $M$.

Subring.matrixdefMathlib.Data.Matrix.Basic, function or constant

Wording

the matrix of S (from the name)

English

Let $S$ be a subring of $R$. Then the matrix of $S$ is a subring of the set of matrixes of $n$ and $R$.

Subsemiring.matrixdefMathlib.Data.Matrix.Basic, function or constant

Wording

the matrix of S (from the name)

English

Let $S$ be a subsemiring of $R$. Then the matrix of $S$ is a subsemiring of the set of matrixes of $n$ and $R$.

Mathlib.Data.Matrix.Basis

Matrix.liftLineardefMathlib.Data.Matrix.Basis, function or constant

Wording

no wording

English

Let $S$ be a set. Then $\operatorname{liftLinear}$ applied to $S$ is a linear equivalence of the set of functions from elements of $m$ and elements of $n$ to linear maps of $x$ and $x_{1}$ and the set of linear maps of the set of matrixes of $n$ and $x$ and $x_{1}$ defined as the composition of the composition of the right product congruence of the function that maps $x_{13}$ to $\operatorname{lsum}$ applied to $R$, the function that maps $x_{14}$ to $x$ and $S$ and $\operatorname{lsum}$ applied to $R$, the function that maps $i$ to the set of functions from elements of $n$ to elements of $x$ and $S$ and the left congruence of the matrix of $R$.

Matrix.singledefMathlib.Data.Matrix.Basis, function or constant

Wording

no wording

English

Let $i$ be an element of $m$. Let $j$ be an element of $n$. Let $a$ be an element of $x$. Then there is a matrix of $n$ and $x$. Proof. Let $i$ be arbitrary. Let $j$ be arbitrary. Let $a$ be arbitrary. Let $\mathrm{i'1}$ be arbitrary. Let $\mathrm{j'1}$ be arbitrary. By i. By i'1. By Eqt. By j. By j'1. By Eqt. By and. By a. By 0. By ite. By Matrix__of__app.

Matrix.singleAddMonoidHomdefMathlib.Data.Matrix.Basis, function or constant

Wording

the single additive monoid homomorphism of i and j (from the name)

English

Let $i$ be an element of $m$. Let $j$ be an element of $n$. Then the single additive monoid homomorphism of $i$ and $j$ is an additive monoid homomorphism of $x$ and the set of matrixes of $n$ and $x$.

Matrix.singleLinearMapdefMathlib.Data.Matrix.Basis, function or constant

Wording

the single linear map of i and j (from the name)

English

Let $R$ be a set. Let $i$ be an element of $m$. Let $j$ be an element of $n$. Then the single linear map of $i$ and $j$ is a linear map of $x$ and the set of matrixes of $n$ and $x$.

Mathlib.Data.Matrix.Block

Matrix.IsTwoBlockDiagonaldefMathlib.Data.Matrix.Block, predicate

Wording

no wording

English

Let $A$ be a matrix of $\mathrm{Sum}$ applied to $l$ and $m$ and $x$. Then $\operatorname{IsTwoBlockDiagonal}$ holds for $A$, if the block of $A$ is equal to $0$ and the block of $A$ is equal to $0$.

Matrix.blockDiagdefMathlib.Data.Matrix.Block, function or constant

Wording

the block diagonal of M and k (from the name)

English

Let $M$ be a matrix of $\mathrm{Prod}$ applied to $n$ and $o$ and $x$. Let $k$ be an element of $o$. Then the block diagonal of $M$ and $k$ is a matrix of $n$ and $x$ defined as $\operatorname{of}$ applied to the function that maps $i_{1}$ and $j_{1}$ to $M$ applied to $\ProdmkMACRoU {i_{1}}{k}$ and $\ProdmkMACRoU {j_{1}}{k}$.

Matrix.blockDiag'defMathlib.Data.Matrix.Block, function or constant

Wording

the block diagonal of M and k (from the name)

English

Let $M$ be a matrix of $\Sigma$ applied to the function that maps $i_{1}$ to $\mathrm{n'}$ applied to $i_{1}$ and $x$. Let $k$ be an element of $o$. Then the block diagonal of $M$ and $k$ is a matrix of $\mathrm{n'}$ applied to $k$ and $x$ defined as $\operatorname{of}$ applied to the function that maps $i_{1}$ and $j_{1}$ to $M$ applied to $\operatorname{mk}$ applied to $k$ and $i_{1}$ and $\operatorname{mk}$ applied to $k$ and $j_{1}$.

Matrix.blockDiag'AddMonoidHomdefMathlib.Data.Matrix.Block, function or constant

Wording

the block diagonal additive monoid homomorphism of x and i2 (from the name)

English

Let $\mathrm{m'}$ and $\mathrm{n'}$ be functions from elements of $o$ to sets. Let $x$ be a set. Then the block diagonal additive monoid homomorphism of $\mathrm{m'}$ and $\mathrm{n'}$ is an additive monoid homomorphism of the set of matrixes of $\Sigma$ applied to the function that maps $i_{1}$ to $\mathrm{n'}$ applied to $i_{1}$ and $x$ and the set of functions from elements $i_{2}$ of $o$ to matrixes of $\mathrm{n'}$ applied to $i_{2}$ and $x$.

Matrix.blockDiagAddMonoidHomdefMathlib.Data.Matrix.Block, function or constant

Wording

the block diagonal additive monoid homomorphism of o and x (from the name)

English

Let $m$, $n$, $o$ and $x$ be sets. Then the block diagonal additive monoid homomorphism of $o$ and $x$ is an additive monoid homomorphism of the set of matrixes of $\mathrm{Prod}$ applied to $n$ and $o$ and $x$ and the set of functions from elements of $o$ to matrixes of $n$ and $x$.

Matrix.blockDiagonaldefMathlib.Data.Matrix.Block, function or constant

Wording

the block diagonal of M (from the name)

English

Let $M$ be a function from elements of $o$ to matrixes of $n$ and $x$. Then the block diagonal of $M$ is a matrix of $\mathrm{Prod}$ applied to $n$ and $o$ and $x$.

Matrix.blockDiagonal'defMathlib.Data.Matrix.Block, function or constant

Wording

the block diagonal of M (from the name)

English

Let $M$ be a function from elements $i_{2}$ of $o$ to matrixes of $\mathrm{n'}$ applied to $i_{2}$ and $x$. Then the block diagonal of $i_{2}$ is a matrix of $\Sigma$ applied to the function that maps $i_{1}$ to $\mathrm{n'}$ applied to $i_{1}$ and $x$.

Matrix.blockDiagonal'AddMonoidHomdefMathlib.Data.Matrix.Block, function or constant

Wording

the block diagonal additive monoid homomorphism of x and i (from the name)

English

Let $\mathrm{m'}$ and $\mathrm{n'}$ be functions from elements of $o$ to sets. Let $x$ be a set. Then the block diagonal additive monoid homomorphism of $\mathrm{m'}$ and $\mathrm{n'}$ is an additive monoid homomorphism of the set of functions from elements $i$ of $o$ to matrixes of $\mathrm{n'}$ applied to $i$ and $x$ and the set of matrixes of $\Sigma$ applied to the function that maps $i_{2}$ to $\mathrm{n'}$ applied to $i_{2}$ and $x$.

Matrix.blockDiagonal'RingHomdefMathlib.Data.Matrix.Block, function or constant

Wording

the block diagonal ring homomorphism of x and i (from the name)

English

Let $\mathrm{m'}$ be a function from elements of $o$ to sets. Let $x$ be a set. Then the block diagonal ring homomorphism of $\mathrm{m'}$ and $x$ is a ring homomorphism of the set of functions from elements $i$ of $o$ to matrixes of $\mathrm{m'}$ applied to $i$ and $x$ and the set of matrixes of $\Sigma$ applied to the function that maps $i_{2}$ to $\mathrm{m'}$ applied to $i_{2}$ and $x$.

Matrix.blockDiagonalAddMonoidHomdefMathlib.Data.Matrix.Block, function or constant

Wording

the block diagonal additive monoid homomorphism of o and x (from the name)

English

Let $m$, $n$, $o$ and $x$ be sets. Then the block diagonal additive monoid homomorphism of $o$ and $x$ is an additive monoid homomorphism of the set of functions from elements of $o$ to matrixes of $n$ and $x$ and the set of matrixes of $\mathrm{Prod}$ applied to $n$ and $o$ and $x$.

Matrix.blockDiagonalRingHomdefMathlib.Data.Matrix.Block, function or constant

Wording

the block diagonal ring homomorphism of o and x (from the name)

English

Let $m$, $o$ and $x$ be sets. Then the block diagonal ring homomorphism of $o$ and $x$ is a ring homomorphism of the set of functions from elements of $o$ to matrixes of $m$ and $x$ and the set of matrixes of $\mathrm{Prod}$ applied to $m$ and $o$ and $x$.

Matrix.fromBlocksdefMathlib.Data.Matrix.Block, function or constant

Wording

no wording

English

Let $A$ and $C$ be matrixes of $l$ and $x$. Let $B$ and $D$ be matrixes of $m$ and $x$. Then there is a matrix of $\mathrm{Sum}$ applied to $l$ and $m$ and $x$. Proof. Let $A$ be arbitrary. Let $B$ be arbitrary. Let $C$ be arbitrary. Let $D$ be arbitrary. Let $i$ be arbitrary. By i. By A. By i. By B. By Sum__elim. Let $j$ be arbitrary. By j. By C. By j. By D. By Sum__elim. By Sum__elim. By Matrix__of__app.

Matrix.toBlockdefMathlib.Data.Matrix.Block, function or constant

Wording

the block of p and q (from the name)

English

Let $M$ be a matrix of $n$ and $x$. Let $p$ be a function from elements of $m$ to propositions. Let $q$ be a function from elements of $n$ to propositions. Then the block of $p$ and $q$ is a matrix of $\SubtypeSet {a_{1}}{q (a_{1})}$ and $x$ defined as the submatrix of the function that maps $a$ to $p$ applied to $a$ and the function that maps $a_{1}$ to $q$ applied to $a_{1}$.

Matrix.toBlocks₁₁defMathlib.Data.Matrix.Block, function or constant

Wording

the block of M (from the name)

English

Let $M$ be a matrix of $\mathrm{Sum}$ applied to $l$ and $m$ and $x$. Then the block of $M$ is a matrix of $l$ and $x$ defined as $\operatorname{of}$ applied to the function that maps $i_{1}$ and $j_{1}$ to $M$ applied to $\operatorname{inl}$ applied to $i_{1}$ and $\operatorname{inl}$ applied to $j_{1}$.

Matrix.toBlocks₁₂defMathlib.Data.Matrix.Block, function or constant

Wording

the block of M (from the name)

English

Let $M$ be a matrix of $\mathrm{Sum}$ applied to $l$ and $m$ and $x$. Then the block of $M$ is a matrix of $m$ and $x$ defined as $\operatorname{of}$ applied to the function that maps $i_{1}$ and $j_{1}$ to $M$ applied to $\operatorname{inl}$ applied to $i_{1}$ and $\operatorname{inr}$ applied to $j_{1}$.

Matrix.toBlocks₂₁defMathlib.Data.Matrix.Block, function or constant

Wording

the block of M (from the name)

English

Let $M$ be a matrix of $\mathrm{Sum}$ applied to $l$ and $m$ and $x$. Then the block of $M$ is a matrix of $l$ and $x$ defined as $\operatorname{of}$ applied to the function that maps $i_{1}$ and $j_{1}$ to $M$ applied to $\operatorname{inr}$ applied to $i_{1}$ and $\operatorname{inl}$ applied to $j_{1}$.

Matrix.toBlocks₂₂defMathlib.Data.Matrix.Block, function or constant

Wording

the block of M (from the name)

English

Let $M$ be a matrix of $\mathrm{Sum}$ applied to $l$ and $m$ and $x$. Then the block of $M$ is a matrix of $m$ and $x$ defined as $\operatorname{of}$ applied to the function that maps $i_{1}$ and $j_{1}$ to $M$ applied to $\operatorname{inr}$ applied to $i_{1}$ and $\operatorname{inr}$ applied to $j_{1}$.

Matrix.toSquareBlockdefMathlib.Data.Matrix.Block, function or constant

Wording

the square block of b and k (from the name)

English

Let $M$ be a matrix of $m$ and $x$. Let $b$ be a function from elements of $m$ to elements of $x_{1}$. Let $k$ be an element of $x_{1}$. Then the square block of $b$ and $k$ is a matrix of $\SubtypeSet {a_{1}}{(\EqtMACRoH {b (a_{1})}{k})}$ and $x$ defined as $\operatorname{toSquareBlockProp}$ applied to $M$ and the function that maps $a$ to $\EqtMACRoH {b (a)}{k}$.

Matrix.toSquareBlockPropdefMathlib.Data.Matrix.Block, function or constant

Wording

no wording

English

Let $M$ be a matrix of $m$ and $x$. Let $p$ be a function from elements of $m$ to propositions. Then there is a matrix of $\SubtypeSet {a_{1}}{p (a_{1})}$ and $x$. Proof. Let $M$ be arbitrary. Let $p$ be arbitrary. By p. By p. By Matrix__toBlock.

Mathlib.Data.Matrix.ColumnRowPartitioned

Matrix.fromColsdefMathlib.Data.Matrix.ColumnRowPartitioned, function or constant

Wording

no wording

English

Let $x_{2}$ be a matrix of $x$ and $R$. Let $x_{3}$ be a matrix of $x_{1}$ and $R$. Then there is a matrix of $\mathrm{Sum}$ applied to $x$ and $x_{1}$ and $R$. Proof. Let $x_{2}$ be arbitrary. Let $x_{3}$ be arbitrary. Let $i_{1}$ be arbitrary. By i1. By x2. By i1. By x3. By Sum__elim. By Matrix__of__app.

Matrix.fromRowsdefMathlib.Data.Matrix.ColumnRowPartitioned, function or constant

Wording

no wording

English

Let $x_{2}$ and $x_{3}$ be matrixes of $n$ and $R$. Then there is a matrix of $n$ and $R$. Proof. Let $x_{2}$ be arbitrary. Let $x_{3}$ be arbitrary. By x2. By x3. By Sum__elim. By Matrix__of__app.

Matrix.toCols₁defMathlib.Data.Matrix.ColumnRowPartitioned, function or constant

Wording

no wording

English

Let $A$ be a matrix of $\mathrm{Sum}$ applied to $x$ and $x_{1}$ and $R$. Then there is a matrix of $x$ and $R$. Proof. Let $A$ be arbitrary. Let $i_{1}$ be arbitrary. Let $j_{1}$ be arbitrary. By i1. By j1. By Sum__inl. By A. By Matrix__of__app.

Matrix.toCols₂defMathlib.Data.Matrix.ColumnRowPartitioned, function or constant

Wording

no wording

English

Let $A$ be a matrix of $\mathrm{Sum}$ applied to $x$ and $x_{1}$ and $R$. Then there is a matrix of $x_{1}$ and $R$. Proof. Let $A$ be arbitrary. Let $i_{1}$ be arbitrary. Let $j_{1}$ be arbitrary. By i1. By j1. By Sum__inr. By A. By Matrix__of__app.

Matrix.toRows₁defMathlib.Data.Matrix.ColumnRowPartitioned, function or constant

Wording

the row of A (from the name)

English

Let $A$ be a matrix of $n$ and $R$. Then the row of $A$ is a matrix of $n$ and $R$ defined as $\operatorname{of}$ applied to the function that maps $i_{1}$ and $j_{1}$ to $A$ applied to $\operatorname{inl}$ applied to $i_{1}$ and $j_{1}$.

Matrix.toRows₂defMathlib.Data.Matrix.ColumnRowPartitioned, function or constant

Wording

the row of A (from the name)

English

Mathlib.Data.Matrix.Composition

Matrix.compdefMathlib.Data.Matrix.Composition, function or constant

Wording

the composition of L and R (from the name)

English

Let $I$, $J$, $K$, $L$ and $R$ be sets. Then the composition of $L$ and $R$ is an equivalence from the set of matrixes of $J$ and the set of matrixes of $L$ and $R$ to the set of matrixes of $\mathrm{Prod}$ applied to $J$ and $L$ and $R$.

Matrix.compAddEquivdefMathlib.Data.Matrix.Composition, function or constant

Wording

the composition additive equivalence of L and R (from the name)

English

Let $I$, $J$, $K$, $L$ and $R$ be sets. Then the composition additive equivalence of $L$ and $R$ is an additive equivalence of the set of matrixes of $J$ and the set of matrixes of $L$ and $R$ and the set of matrixes of $\mathrm{Prod}$ applied to $J$ and $L$ and $R$.

Matrix.compAlgEquivdefMathlib.Data.Matrix.Composition, function or constant

Wording

the composition algebra isomorphism of R and K (from the name)

English

Let $I$, $J$, $R$ and $K$ be sets. Then the composition algebra isomorphism of $R$ and $K$ is an algebra isomorphism of the set of matrixes of $I$ and the set of matrixes of $J$ and $R$ and the set of matrixes of $\mathrm{Prod}$ applied to $I$ and $J$ and $R$.

Matrix.compLinearEquivdefMathlib.Data.Matrix.Composition, function or constant

Wording

the composition linear equivalence of R and x (from the name)

English

Let $I$, $J$, $K$, $L$, $R$ and $x$ be sets. Then the composition linear equivalence of $R$ and $x$ is a linear equivalence of the set of matrixes of $J$ and the set of matrixes of $L$ and $R$ and the set of matrixes of $\mathrm{Prod}$ applied to $J$ and $L$ and $R$.

Matrix.compRingEquivdefMathlib.Data.Matrix.Composition, function or constant

Wording

the composition ring isomorphism of J and R (from the name)

English

Let $I$, $J$ and $R$ be sets. Then the composition ring isomorphism of $J$ and $R$ is a ring isomorphism of the set of matrixes of $I$ and the set of matrixes of $J$ and $R$ and the set of matrixes of $\mathrm{Prod}$ applied to $I$ and $J$ and $R$.

Mathlib.Data.Matrix.DMatrix

AddMonoidHom.mapDMatrixdefMathlib.Data.Matrix.DMatrix, function or constant

Wording

the map matrix of f (from the name)

English

Let $f$ be a function from elements $i$ of $m$ and elements $j$ of $n$ to additive monoid homomorphisms of $x$ applied to $i$ and $j$ and $x_{2}$ applied to $i$ and $j$. Then the map matrix of $i$ is an additive monoid homomorphism of the set of matrixes of $n$ and $x$ and the set of matrixes of $n$ and $x_{2}$.

DMatrixdefMathlib.Data.Matrix.DMatrix, type

Wording

matrix of n and x (from the name)

English

Let $m$ and $n$ be sets. Let $x$ be a function from elements of $m$ and elements of $n$ to sets. Then a matrix of $n$ and $x$ is an element of the function that maps $m$, $n$ and $x$ to the set of functions from elements $i$ of $m$ and elements $j$ of $n$ to elements of $x$ applied to $i$ and $j$.

DMatrix.coldefMathlib.Data.Matrix.DMatrix, function or constant

Wording

no wording

English

Let $w$ be a function from elements $i_{1}$ of $m$ to elements of $x$ applied to $i_{1}$. Then there is a matrix of $\mathrm{Unit}$ and the function that maps $i$ and $\mathrm{\_j}$ to $x$ applied to $i$.

DMatrix.mapdefMathlib.Data.Matrix.DMatrix, function or constant

Wording

the map of M and f (from the name)

English

Let $M$ be a matrix of $n$ and $x$. Let $f$ be a function from elements $i$ of $m$ and elements $j$ of $n$ and elements of $x$ applied to $i$ and $j$ to elements of $x_{1}$ applied to $i$ and $j$. Then the map of $M$ and $i$ is a matrix of $n$ and $x_{1}$ defined as the function that maps $i$ and $j$ to $i$ applied to $j$, $f$ and $M$ applied to $j$ and $f$.

DMatrix.rowdefMathlib.Data.Matrix.DMatrix, function or constant

Wording

the row of v (from the name)

English

Let $v$ be a function from elements $j_{1}$ of $n$ to elements of $x$ applied to $j_{1}$. Then the row of $j_{1}$ is a matrix of $n$ and the function that maps $\mathrm{\_i}$ and $j$ to $x$ applied to $j$.

DMatrix.transposedefMathlib.Data.Matrix.DMatrix, function or constant

Wording

the transpose of M (from the docstring)

English

Let $M$ be a matrix of $n$ and $x$. Then the transpose of $M$ is a matrix of $m$ and the function that maps $j$ and $i$ to $x$ applied to $i$ and $j$.

Mathlib.Data.Matrix.Diagonal

Matrix.diagdefMathlib.Data.Matrix.Diagonal, function or constant

Wording

the diagonal of A and i (from the docstring)

English

Let $A$ be a matrix of $n$ and $x$. Let $i$ be an element of $n$. Then the diagonal of $A$ and $i$ is an element of $x$ defined as $A$ applied to $i$ and $i$.

Matrix.diagonaldefMathlib.Data.Matrix.Diagonal, function or constant

Wording

the diagonal of d (from the name)

English

Let $d$ be a function from elements of $n$ to elements of $x$. Then the diagonal of $d$ is a matrix of $n$ and $x$ defined as $\operatorname{of}$ applied to the function that maps $i_{1}$ and $j_{1}$ to $\iteMACRoG {(\EqtMACRoH {i_{1}}{j_{1}})}{d (i_{1})}{0}$.

Mathlib.Data.Matrix.Mul

IsStablyFiniteRingclassMathlib.Data.Matrix.Mul, predicate

Wording

R is stably finite (from the docstring)

English

generation took over the time limit

Matrix.addMonoidHomMulLeftdefMathlib.Data.Matrix.Mul, function or constant

Wording

the left additive monoid homomorphism multiplicative of M (from the name)

English

Let $M$ be a matrix of $m$ and $x$. Then the left additive monoid homomorphism multiplicative of $M$ is an additive monoid homomorphism of the set of matrixes of $n$ and $x$ and the set of matrixes of $n$ and $x$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the function that maps $x_{3}$ to $M \times x_{3}$ and $\mathrm{Matrix\_\_mul\_zero}$ applied to $M$ and $\mathrm{Matrix\_\_mul\_add}$ applied to $M$.

Matrix.addMonoidHomMulRightdefMathlib.Data.Matrix.Mul, function or constant

Wording

the right additive monoid homomorphism multiplicative of M (from the name)

English

Let $M$ be a matrix of $n$ and $x$. Then the right additive monoid homomorphism multiplicative of $M$ is an additive monoid homomorphism of the set of matrixes of $m$ and $x$ and the set of matrixes of $n$ and $x$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the function that maps $x_{3}$ to $x_{3} \times M$ and $\mathrm{Matrix\_\_zero\_mul}$ applied to $M$ and the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Matrix\_\_add\_mul}$ applied to $x_{4}$, $x_{5}$ and $M$.

Matrix.mulVecdefMathlib.Data.Matrix.Mul, function or constant

Wording

the multiplicative vector of v and x3 (from the name)

English

Let $M$ be a matrix of $n$ and $x$. Let $v$ be a function from elements of $n$ to elements of $x$. Let $x_{3}$ be an element of $m$. Then the multiplicative vector of $v$ and $x_{3}$ is an element of $x$ defined as the sum of the entrywise products of the function that maps $j$ to $M$ applied to $x_{3}$ and $j$ and $v$.

Matrix.mulVec.addMonoidHomLeftdefMathlib.Data.Matrix.Mul, function or constant

Wording

the left additive monoid homomorphism of v (from the name)

English

Let $v$ be a function from elements of $n$ to elements of $x$. Then the left additive monoid homomorphism of $v$ is an additive monoid homomorphism of the set of matrixes of $n$ and $x$ and the set of functions from elements of $m$ to elements of $x$.

Matrix.vecMuldefMathlib.Data.Matrix.Mul, function or constant

Wording

the vector product of M and x3 (from the name)

English

Let $v$ be a function from elements of $m$ to elements of $x$. Let $M$ be a matrix of $n$ and $x$. Let $x_{3}$ be an element of $n$. Then the vector product of $M$ and $x_{3}$ is an element of $x$ defined as the sum of the entrywise products of $v$ and the function that maps $i$ to $M$ applied to $i$ and $x_{3}$.

Matrix.vecMulVecdefMathlib.Data.Matrix.Mul, function or constant

Wording

the vector multiplicative vector of w and v (from the name)

English

Let $w$ be a function from elements of $m$ to elements of $x$. Let $v$ be a function from elements of $n$ to elements of $x$. Then the vector multiplicative vector of $w$ and $v$ is a matrix of $n$ and $x$ defined as $\operatorname{of}$ applied to the function that maps $x_{3}$ and $y_{1}$ to $w (x_{3})\times v (y_{1})$.

dotProductdefMathlib.Data.Matrix.Mul, function or constant

Wording

the sum of the entrywise products of v and w (from the docstring)

English

Let $v$ and $w$ be functions from elements of $m$ to elements of $x$. Then the sum of the entrywise products of $v$ and $w$ is an element of $x$ defined as $\FinsetSum {\FinsetunivMACRoAC}{i}{(v (i)\times w (i))}$.

Mathlib.Data.Matrix.PEquiv

PEquiv.toMatrixdefMathlib.Data.Matrix.PEquiv, function or constant

Wording

the matrix of f (from the name)

English

Let $f$ be an equivalence of $m$ and $n$. Then the matrix of $f$ is a matrix of $n$ and $x$ defined as $\operatorname{of}$ applied to the function that maps $i_{1}$ and $j_{1}$ to $\iteMACRoG {(\MembershipmemMACRoT {f (i_{1})}{j_{1}})}{1}{0}$.

Mathlib.Data.Matrix.Reflection

Matrix.ExistsdefMathlib.Data.Matrix.Reflection, predicate

Wording

no wording

English

Let $x_{1}$ be a function from matrixes of $\mathrm{Fin}$ applied to $n$ and $x$ to propositions. Then $\operatorname{Exists}$ holds for $x_{1}$, if $\operatorname{brecOn}$ holds for $m$, $\mathrm{Matrix\_\_Exists\_\_\_f}$, $n$ and $x_{1}$.

Matrix.ForalldefMathlib.Data.Matrix.Reflection, predicate

Wording

no wording

English

Let $x_{1}$ be a function from matrixes of $\mathrm{Fin}$ applied to $n$ and $x$ to propositions. Then $\operatorname{Forall}$ holds for $x_{1}$, if $\operatorname{brecOn}$ holds for $m$, $\mathrm{Matrix\_\_Forall\_\_\_f}$, $n$ and $x_{1}$.

Matrix.dotProductᵣdefMathlib.Data.Matrix.Reflection, function or constant

Wording

the dot product of a and b (from the name)

English

Let $a$ and $b$ be functions from elements of $\mathrm{Fin}$ applied to $m$ to elements of $x$. Then the dot product of $a$ and $b$ is an element of $x$ defined as the sum of $\operatorname{seq}$ applied to $b$.

Matrix.etaExpanddefMathlib.Data.Matrix.Reflection, function or constant

Wording

no wording

English

Let $A$ be a matrix of $\mathrm{Fin}$ applied to $n$ and $x$. Then there is a matrix of $\mathrm{Fin}$ applied to $n$ and $x$. Proof. Let $A$ be arbitrary. Let $i$ be arbitrary. Let $j$ be arbitrary. By i. By j. By A. By FinVec__etaExpand. By FinVec__etaExpand. By Matrix__of__app.

Matrix.mulVecᵣdefMathlib.Data.Matrix.Reflection, function or constant

Wording

the multiplicative vector of v and x4 (from the name)

English

Let $A$ be a matrix of $\mathrm{Fin}$ applied to $m$ and $x$. Let $v$ be a function from elements of $\mathrm{Fin}$ applied to $m$ to elements of $x$. Let $x_{4}$ be an element of $\mathrm{Fin}$ applied to $l$. Then the multiplicative vector of $v$ and $x_{4}$ is an element of $x$ defined as the map of $A$ and $x_{4}$.

Matrix.mulᵣdefMathlib.Data.Matrix.Reflection, function or constant

Wording

the product of A and B (from the name)

English

Let $A$ be a matrix of $\mathrm{Fin}$ applied to $m$ and $x$. Let $B$ be a matrix of $\mathrm{Fin}$ applied to $n$ and $x$. Then the product of $A$ and $B$ is a matrix of $\mathrm{Fin}$ applied to $n$ and $x$ defined as $\operatorname{of}$ applied to $\operatorname{map}$ applied to $A$.

Matrix.transposeᵣdefMathlib.Data.Matrix.Reflection, function or constant

Wording

the transpose of x1 (from the name)

English

Let $x_{1}$ be a matrix of $\mathrm{Fin}$ applied to $n$ and $x$. Then the transpose of $x_{1}$ is a matrix of $\mathrm{Fin}$ applied to $m$ and $x$ defined as $\operatorname{brecOn}$ applied to $n$, $\mathrm{Matrix\_\_transpose\_u1d63\_\_\_\_f}$, $m$ and $x_{1}$.

Matrix.vecMulᵣdefMathlib.Data.Matrix.Reflection, function or constant

Wording

the vector product of A and x4 (from the name)

English

Let $v$ be a function from elements of $\mathrm{Fin}$ applied to $l$ to elements of $x$. Let $A$ be a matrix of $\mathrm{Fin}$ applied to $m$ and $x$. Let $x_{4}$ be an element of $\mathrm{Fin}$ applied to $m$. Then the vector product of $A$ and $x_{4}$ is an element of $x$ defined as the map of the transpose of $A$ and $x_{4}$.

Mathlib.Data.Multiset.AddSub

Multiset.adddefMathlib.Data.Multiset.AddSub, function or constant

Wording

the sum of x1 and x2 (from the name)

English

Let $x_{1}$ and $x_{2}$ be multisets of $x$. Then the sum of $x_{1}$ and $x_{2}$ is a multiset of $x$.

Multiset.erasedefMathlib.Data.Multiset.AddSub, function or constant

Wording

no wording

English

Let $s$ be a multiset of $x$. Let $a$ be an element of $x$. Then $\operatorname{erase}$ applied to $s$ and $a$ is a multiset of $x$.

Multiset.subdefMathlib.Data.Multiset.AddSub, function or constant

Wording

the difference of s and t (from the name)

English

Let $s$ and $t$ be multisets of $x$. Then the difference of $s$ and $t$ is a multiset of $x$.

Mathlib.Data.Multiset.Antidiagonal

Multiset.antidiagonaldefMathlib.Data.Multiset.Antidiagonal, function or constant

Wording

no wording

English

Let $s$ be a multiset of $x$. Then $\operatorname{antidiagonal}$ applied to $s$ is a multiset of $\mathrm{Prod}$ applied to the set of multisets of $x$ and the set of multisets of $x$.

Mathlib.Data.Multiset.Basic

Multiset.choosedefMathlib.Data.Multiset.Basic, function or constant

Wording

no wording

English

Let $p$ be a function from elements of $x$ to propositions. Let $l$ be a multiset of $x$ such that $\mathrm{ExistsUnique}$ holds for the function that maps $a$ to the proposition that $a$ is an element of $l$ and $p$ holds for $a$. Then $\operatorname{choose}$ applied to $p$, $l$ and $\mathrm{hp}$ is an element of $x$ defined as $\operatorname{chooseX}$ applied to $p$, $l$ and $\mathrm{hp}$.

Multiset.chooseXdefMathlib.Data.Multiset.Basic, function or constant

Wording

no wording

English

Let $p$ be a function from elements of $x$ to propositions. Let $l$ be a multiset of $x$ such that $\mathrm{ExistsUnique}$ holds for the function that maps $a_{1}$ to the proposition that $a_{1}$ is an element of $l$ and $p$ holds for $a_{1}$. Then $\operatorname{chooseX}$ applied to $p$, $l$ and $\mathrm{\_hp}$ is an element of $\SubtypeSet {a}{\mathrm{and} (\MembershipmemMACRoT {l}{a}, p (a))}$.

Multiset.strongDownwardInductiondefMathlib.Data.Multiset.Basic, function or constant

Wording

the strong downward induction of H and x1 (from the name)

English

Let $H$ be a function from multisets $x_{1}$ of $x$ and functions from multisets $x_{3}$ of $x$ and elements of $\mathrm{Proof}$ applied to the proposition that the cardinality of $x_{3}$ is less than or equal to $n$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (x_{1} , x_{3})$ to elements of $p$ applied to $x_{3}$ and elements of $\mathrm{Proof}$ applied to the proposition that the cardinality of $x_{1}$ is less than or equal to $n$ to elements of $p$ applied to $x_{1}$. Let $s$ be a multiset of $x$ such that the cardinality of $s$ is less than or equal to $n$. Then the strong downward induction of $x_{1}$ and $H$ is an element of $p$ applied to $s$.

Multiset.strongDownwardInductionOndefMathlib.Data.Multiset.Basic, function or constant

Wording

no wording

English

Let $s$ be a multiset of $x$. Let $x_{1}$ be a function from multisets $x_{2}$ of $x$ and functions from multisets $x_{4}$ of $x$ and elements of $\mathrm{Proof}$ applied to the proposition that the cardinality of $x_{4}$ is less than or equal to $n$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (x_{2} , x_{4})$ to elements of $p$ applied to $x_{4}$ and elements of $\mathrm{Proof}$ applied to the proposition that the cardinality of $x_{2}$ is less than or equal to $n$ to elements of $p$ applied to $x_{2}$. Assume that the cardinality of $s$ is less than or equal to $n$. Then $\operatorname{strongDownwardInductionOn}$ applied to $s$, $x_{2}$, $x_{1}$ and $h$ is an element of $p$ applied to $s$ defined as the function that maps $h$ to the strong downward induction of $x_{2}$ and $s$.

Multiset.strongInductionOndefMathlib.Data.Multiset.Basic, function or constant

Wording

no wording

English

Let $s$ be a multiset of $x$. Let $\mathrm{ih}$ be a function from multisets $s_{1}$ of $x$ and functions from multisets $t$ of $x$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (t , s_{1})$ to elements of $p$ applied to $t$ to elements of $p$ applied to $s_{1}$. Then $\operatorname{strongInductionOn}$ applied to $s$, $s_{1}$ and $\mathrm{ih}$ is an element of $p$ applied to $s$ defined as the function that maps $\mathrm{ih}$ to $\mathrm{Multiset\_\_strongInductionOn\_\_\_unary}$ applied to $s_{1}$, $s$ and $\mathrm{ih}$.

Multiset.subsingletonEquivdefMathlib.Data.Multiset.Basic, function or constant

Wording

the subsingleton equivalence of x (from the name)

English

Let $x$ be a set. Then the subsingleton equivalence of $x$ is an equivalence from the set of lists of elements of $x$ to the set of multisets of $x$.

Multiset.toListdefMathlib.Data.Multiset.Basic, function or constant

Wording

the list of s (from the name)

English

Let $s$ be a multiset of $x$. Then the list of $s$ is a list of elements of $x$ defined as $\operatorname{out}$ applied to $s$.

Mathlib.Data.Multiset.Bind

Multiset.binddefMathlib.Data.Multiset.Bind, function or constant

Wording

no wording

English

Let $s$ be a multiset of $x$. Let $f$ be a function from elements of $x$ to multisets of $x_{1}$. Then $\operatorname{bind}$ applied to $s$ and $f$ is a multiset of $x_{1}$ defined as the join of the map of $f$ and $s$.

Multiset.joindefMathlib.Data.Multiset.Bind, function or constant

Wording

the join of x1 (from the name)

English

Let $x_{1}$ be a multiset of the set of multisets of $x$. Then the join of $x_{1}$ is a multiset of $x$ defined as the sum of $x_{1}$.

Multiset.productdefMathlib.Data.Multiset.Bind, function or constant

Wording

the product of s and t (from the name)

English

Let $s$ be a multiset of $x$. Let $t$ be a multiset of $x_{1}$. Then the product of $s$ and $t$ is a multiset of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ defined as $\operatorname{bind}$ applied to $s$ and the function that maps $a$ to the map of $\ProdmkMACRoU {a}$ and $t$.

Multiset.sigmadefMathlib.Data.Multiset.Bind, function or constant

Wording

the sigma of s and t (from the name)

English

Let $s$ be a multiset of $x$. Let $t$ be a function from elements $a_{1}$ of $x$ to multisets of $x_{1}$ applied to $a_{1}$. Then the sigma of $s$ and $a_{1}$ is a multiset of $\Sigma$ applied to the function that maps $a$ to $x_{1}$ applied to $a$ defined as the function that maps $t$ to $\operatorname{bind}$ applied to $s$, the function that maps $a$ to the map of $\operatorname{mk}$ applied to $a$ and $a_{1}$ applied to $a$ and $t$.

Mathlib.Data.Multiset.Count

Multiset.countdefMathlib.Data.Multiset.Count, function or constant

Wording

the count of a and x2 (from the name)

English

Let $a$ be an element of $x$. Let $x_{2}$ be a multiset of $x$. Then the count of $a$ and $x_{2}$ is a natural number defined as the count of the function that maps $x_{2}$ to $\EqtMACRoH {a}{x_{2}}$ and $x_{2}$.

Multiset.countPdefMathlib.Data.Multiset.Count, function or constant

Wording

the count of p and s (from the name)

English

Let $p$ be a function from elements of $x$ to propositions. Let $s$ be a multiset of $x$. Then the count of $p$ and $s$ is a natural number.

Mathlib.Data.Multiset.Dedup

Multiset.dedupdefMathlib.Data.Multiset.Dedup, function or constant

Wording

no wording

English

Let $s$ be a multiset of $x$. Then $\operatorname{dedup}$ applied to $s$ is a multiset of $x$.

Mathlib.Data.Multiset.Defs

MultisetdefMathlib.Data.Multiset.Defs, type

Wording

multiset of x (from the name)

English

Let $x$ be a set. Then a multiset of $x$ is an element of the function that maps $x$ to $\mathrm{Quotient}$ applied to $\operatorname{isSetoid}$ applied to $x$.

Multiset.LedefMathlib.Data.Multiset.Defs, predicate

Wording

no wording

English

Let $s$ and $t$ be multisets of $x$. Then we can say that $\operatorname{Le}$ holds for $s$ and $t$.

Multiset.MemdefMathlib.Data.Multiset.Defs, predicate

Wording

no wording

English

Let $s$ be a multiset of $x$. Let $a$ be an element of $x$. Then we can say that $\operatorname{Mem}$ holds for $s$ and $a$.

Multiset.NodupdefMathlib.Data.Multiset.Defs, predicate

Wording

no wording

English

Let $s$ be a multiset of $x$. Then we can say that $\operatorname{Nodup}$ holds for $s$.

Multiset.PairwisedefMathlib.Data.Multiset.Defs, predicate

Wording

no wording

English

Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $m$ be a multiset of $x$. Then $\operatorname{Pairwise}$ holds for $r$ and $m$, if there exists a list $l$ of elements of $x$, such that $m$ is equal to the multiset of $l$ and $\operatorname{Pairwise}$ holds for $r$ and $l$.

Multiset.SubsetdefMathlib.Data.Multiset.Defs, predicate

Wording

no wording

English

Let $s$ and $t$ be multisets of $x$. Then $\operatorname{Subset}$ holds for $s$ and $t$, if for all elements $a$ of $x$, if $a$ is an element of $s$, then $a$ is an element of $t$.

Multiset.attachdefMathlib.Data.Multiset.Defs, function or constant

Wording

no wording

English

Let $s$ be a multiset of $x$. Then $\operatorname{attach}$ applied to $s$ is a multiset of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {s}{x_{1}})}$.

Multiset.carddefMathlib.Data.Multiset.Defs, function or constant

Wording

the cardinality of x1 (from the docstring)

English

Let $x_{1}$ be a multiset of $x$. Then the cardinality of $x_{1}$ is a natural number defined as $\operatorname{lift}$ applied to $\operatorname{length}$, the function that maps $x_{1}$ and $x_{2}$ to $\mathrm{List\_\_Perm\_\_length\_eq}$ and $x_{1}$.

Multiset.ofListdefMathlib.Data.Multiset.Defs, function or constant

Wording

the multiset of x1 (from the name)

English

Let $x_{1}$ be a list of elements of $x$. Then the multiset of $x_{1}$ is a multiset of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{r}$ and $x_{1}$.

Multiset.pmapdefMathlib.Data.Multiset.Defs, function or constant

Wording

no wording

English

Let $f$ be a function from elements $a_{1}$ of $x$ and elements of $\mathrm{Proof}$ applied to $p$ applied to $a_{1}$ to elements of $x_{1}$. Let $s$ be a multiset of $x$ such that for all elements $a$ of $x$, if $a$ is an element of $s$, then $p$ holds for $a$. Then $\operatorname{pmap}$ applied to $a_{1}$, $f$, $s$ and $h$ is a multiset of $x_{1}$.

Mathlib.Data.Multiset.DershowitzManna

Multiset.IsDershowitzMannaLTdefMathlib.Data.Multiset.DershowitzManna, predicate

Wording

no wording

English

Let $M$ and $N$ be multisets of $x$. Then $\operatorname{IsDershowitzMannaLT}$ holds for $M$ and $N$, if there exist multisets $X$, $Y$ and $Z$ of $x$, such that $Z \neq \operatorname{emptyCollection}$, $\EqtMACRoH {M}{X + Y}$, $\EqtMACRoH {N}{X + Z}$ and for all elements $y$ of $x$, if $y$ is an element of $Y$, then there exists an element $z$ of $x$ such that $z$ is an element of $Z$ and $y < z$.

Mathlib.Data.Multiset.Filter

Multiset.filterdefMathlib.Data.Multiset.Filter, function or constant

Wording

the filter of p and s (from the name)

English

Let $p$ be a function from elements of $x$ to propositions. Let $s$ be a multiset of $x$. Then the filter of $p$ and $s$ is a multiset of $x$.

Multiset.filterMapdefMathlib.Data.Multiset.Filter, function or constant

Wording

the filter map of f and s (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $\mathrm{Option}$ applied to $x_{1}$. Let $s$ be a multiset of $x$. Then the filter map of $f$ and $s$ is a multiset of $x_{1}$.

Multiset.mapEmbeddingdefMathlib.Data.Multiset.Filter, function or constant

Wording

the map embedding of f (from the name)

English

Let $f$ be an embedding of $x$ and $x_{1}$. Then the map embedding of $f$ is an order embedding of the set of multisets of $x$ and the set of multisets of $x_{1}$.

Mathlib.Data.Multiset.Find

Multiset.find?defMathlib.Data.Multiset.Find, function or constant

Wording

no wording

English

Let $p$ be a function from elements of $x$ to propositions. Let $s$ be a multiset of $x$ such that $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to the proposition that $x_{2}$ is an element of $s$ and $p$ holds for $x_{2}$ is a subsingleton. Then $\mathrm{Multiset\_\_find?}$ applied to $p$, $s$ and $h$ is an element of $\mathrm{Option}$ applied to $x$.

Mathlib.Data.Multiset.FinsetOps

Multiset.ndinsertdefMathlib.Data.Multiset.FinsetOps, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Let $s$ be a multiset of $x$. Then $\operatorname{ndinsert}$ applied to $a$ and $s$ is a multiset of $x$.

Multiset.ndinterdefMathlib.Data.Multiset.FinsetOps, function or constant

Wording

no wording

English

Let $s$ and $t$ be multisets of $x$. Then $\operatorname{ndinter}$ applied to $s$ and $t$ is a multiset of $x$ defined as the filter of the function that maps $x_{2}$ to $\MembershipmemMACRoT {t}{x_{2}}$ and $s$.

Multiset.nduniondefMathlib.Data.Multiset.FinsetOps, function or constant

Wording

no wording

English

Let $s$ and $t$ be multisets of $x$. Then $\operatorname{ndunion}$ applied to $s$ and $t$ is a multiset of $x$.

Mathlib.Data.Multiset.Fintype

Multiset.castdefMathlib.Data.Multiset.Fintype, function or constant

Wording

the cast of h (from the name)

English

Assume that $\EqtMACRoH {s}{t}$. Then the cast of $h$ is an element of $\EquivMACRoAE {\operatorname{ToType} (s)}{\operatorname{ToType} (t)}$.

Multiset.coeEmbeddingdefMathlib.Data.Multiset.Fintype, function or constant

Wording

the embedding of m (from the docstring)

English

Let $m$ be a multiset of $x$. Then the embedding of $m$ is an embedding of $\operatorname{ToType}$ applied to $m$ and $\mathrm{Prod}$ applied to $x$ and $\Natural$.

Multiset.coeEquivdefMathlib.Data.Multiset.Fintype, function or constant

Wording

the coercion equivalence of m (from the name)

English

Let $m$ be a multiset of $x$. Then the coercion equivalence of $m$ is an element of $\EquivMACRoAE {\operatorname{ToType} (m)}{(\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{toEnumFinset} (m)}{x_{2}})})}$.

Multiset.consEquivdefMathlib.Data.Multiset.Fintype, function or constant

Wording

no wording

English

$\operatorname{consEquiv}$ is an element of $\EquivMACRoAE {\operatorname{ToType} (\operatorname{cons} (v , m))}{\mathrm{Option} (\operatorname{ToType} (m))}$.

Multiset.mapEquivdefMathlib.Data.Multiset.Fintype, function or constant

Wording

the map equivalence of s and f (from the name)

English

Let $s$ be a multiset of $x$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the map equivalence of $s$ and $f$ is an equivalence from $\operatorname{ToType}$ applied to $s$ to $\operatorname{ToType}$ applied to the map of $f$ and $s$ defined as $\operatorname{out}$ applied to $\operatorname{mapEquivAux}$ applied to $s$ and $f$.

Multiset.mkToTypedefMathlib.Data.Multiset.Fintype, function or constant

Wording

no wording

English

Let $m$ be a multiset of $x$. Let $x_{2}$ be an element of $x$. Let $i$ be an element of $\mathrm{Fin}$ applied to the count of $x_{2}$ and $m$. Then $\operatorname{mkToType}$ applied to $m$, $x_{2}$ and $i$ is an element of $\operatorname{ToType}$ applied to $m$ defined as $\operatorname{mk}$ applied to $x_{2}$ and $i$.

Multiset.toEnumFinsetdefMathlib.Data.Multiset.Fintype, function or constant

Wording

no wording

English

Let $m$ be a multiset of $x$. Then $\operatorname{toEnumFinset}$ applied to $m$ is a finite set of $\mathrm{Prod}$ applied to $x$ and $\Natural$ defined as the finite set of $\operatorname{ofPred}$ applied to the function that maps $p$ to the proposition that $\ProdsndMACRoAA {p}$ is less than the count of $\ProdfstMACRoZ {p}$ and $m$.

Mathlib.Data.Multiset.Fold

Multiset.folddefMathlib.Data.Multiset.Fold, function or constant

Wording

the fold of x1 and x2 (from the name)

English

Let $\mathrm{op}$ be a function from elements of $x$ and elements of $x$ to elements of $x$. Let $x_{1}$ be an element of $x$. Let $x_{2}$ be a multiset of $x$. Then the fold of $x_{1}$ and $x_{2}$ is an element of $x$ defined as $\operatorname{foldr}$ applied to $\mathrm{op}$, $x_{1}$ and $x_{2}$.

Mathlib.Data.Multiset.Functor

Multiset.traversedefMathlib.Data.Multiset.Functor, function or constant

Wording

the traverse of f and x3 (from the name)

English

Let $f$ be a function from elements of $x_{1}$ to elements of $F$ applied to $x_{2}$. Let $x_{3}$ be a multiset of $x_{1}$. Then the traverse of $f$ and $x_{3}$ is an element of $F$ applied to the set of multisets of $x_{2}$.

Mathlib.Data.Multiset.Lattice

Multiset.infdefMathlib.Data.Multiset.Lattice, function or constant

Wording

the infimum of s (from the name)

English

Let $s$ be a multiset of $x$. Then the infimum of $s$ is an element of $x$ defined as the fold of the top and $s$.

Multiset.supdefMathlib.Data.Multiset.Lattice, function or constant

Wording

the supremum of s (from the name)

English

Let $s$ be a multiset of $x$. Then the supremum of $s$ is an element of $x$ defined as the fold of the bottom and $s$.

Mathlib.Data.Multiset.MapFold

Multiset.foldldefMathlib.Data.Multiset.MapFold, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $x_{1}$ and elements of $x$ to elements of $x_{1}$. Let $b$ be an element of $x_{1}$. Let $s$ be a multiset of $x$. Then $\operatorname{foldl}$ applied to $f$, $b$ and $s$ is an element of $x_{1}$ defined as $\operatorname{liftOn}$ applied to $s$, the function that maps $l$ to $\operatorname{foldl}$ applied to $f$, $b$ and $l$ and the function that maps $x_{2}$, $x_{3}$ and $p$ to $\mathrm{List\_\_Perm\_\_foldl\_eq}$ applied to $p$ and $b$.

Multiset.foldrdefMathlib.Data.Multiset.MapFold, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{1}$. Let $b$ be an element of $x_{1}$. Let $s$ be a multiset of $x$. Then $\operatorname{foldr}$ applied to $f$, $b$ and $s$ is an element of $x_{1}$ defined as $\operatorname{liftOn}$ applied to $s$, the function that maps $l$ to $\operatorname{foldr}$ applied to $f$, $b$ and $l$ and the function that maps $x_{2}$, $x_{3}$ and $p$ to $\mathrm{List\_\_Perm\_\_foldr\_eq}$ applied to $p$ and $b$.

Multiset.mapdefMathlib.Data.Multiset.MapFold, function or constant

Wording

the map of f and s (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be a multiset of $x$. Then the map of $f$ and $s$ is a multiset of $x_{1}$.

Mathlib.Data.Multiset.NatAntidiagonal

Multiset.Nat.antidiagonaldefMathlib.Data.Multiset.NatAntidiagonal, function or constant

Wording

no wording

English

Let $n$ be a natural number. Then $\operatorname{antidiagonal}$ applied to $n$ is a multiset of $\mathrm{Prod}$ applied to $\Natural$ and $\Natural$ defined as the multiset of $\operatorname{antidiagonal}$ applied to $n$.

Mathlib.Data.Multiset.Pi

Multiset.Pi.consdefMathlib.Data.Multiset.Pi, function or constant

Wording

no wording

English

Let $m$ be a multiset of $x$. Let $a$ and $\mathrm{a'}$ be elements of $x$. Let $b$ be an element of $x_{2}$ applied to $a$. Let $f$ be a function from elements $a_{1}$ of $x$ and elements of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {m}{a_{1}}$ to elements of $x_{2}$ applied to $a_{1}$. Assume that $\MembershipmemMACRoT {\operatorname{cons} (a , m)}{\mathrm{a'}}$. Then $\operatorname{cons}$ applied to $m$, $a$, $b$, $a_{1}$, $f$, $\mathrm{a'}$ and $h$ is an element of $x_{2}$ applied to $\mathrm{a'}$.

Multiset.Pi.emptydefMathlib.Data.Multiset.Pi, function or constant

Wording

no wording

English

Let $x_{1}$ be a function from elements of $x$ to sets. Let $a$ be an element of $x$ such that $a$ is an element of $0$. Then $\operatorname{empty}$ applied to $x_{1}$, $a$ and $h$ is an element of $x_{1}$ applied to $a$.

Multiset.pidefMathlib.Data.Multiset.Pi, function or constant

Wording

the product of m and t (from the name)

English

Let $m$ be a multiset of $x$. Let $t$ be a function from elements $a_{1}$ of $x$ to multisets of $x_{2}$ applied to $a_{1}$. Then the product of $m$ and $a_{1}$ is a multiset of the set of functions from elements $a$ of $x$ and elements of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {m}{a}$ to elements of $x_{2}$ applied to $a$.

Mathlib.Data.Multiset.Powerset

Multiset.powersetdefMathlib.Data.Multiset.Powerset, function or constant

Wording

the power set of s (from the docstring)

English

Let $s$ be a multiset of $x$. Then the power set of $s$ is a multiset of the set of multisets of $x$.

Multiset.powersetAux'defMathlib.Data.Multiset.Powerset, function or constant

Wording

the powerset of l (from the name)

English

Let $l$ be a list of elements of $x$. Then the powerset of $l$ is a list of multisets of $x$ defined as $\operatorname{map}$ applied to $\operatorname{ofList}$ and $\operatorname{sublists'}$ applied to $l$.

Multiset.powersetCarddefMathlib.Data.Multiset.Powerset, function or constant

Wording

the powerset cardinality of n and s (from the name)

English

Let $n$ be a natural number. Let $s$ be a multiset of $x$. Then the powerset cardinality of $n$ and $s$ is a multiset of the set of multisets of $x$.

Mathlib.Data.Multiset.Range

Multiset.rangedefMathlib.Data.Multiset.Range, function or constant

Wording

the range of n (from the name)

English

Let $n$ be a natural number. Then the range of $n$ is a multiset of $\Natural$ defined as the multiset of $\operatorname{range}$ applied to $n$.

Mathlib.Data.Multiset.Replicate

Multiset.replicatedefMathlib.Data.Multiset.Replicate, function or constant

Wording

no wording

English

Let $n$ be a natural number. Let $a$ be an element of $x$. Then $\operatorname{replicate}$ applied to $n$ and $a$ is a multiset of $x$ defined as the multiset of $\operatorname{replicate}$ applied to $n$ and $a$.

Mathlib.Data.Multiset.Sections

Multiset.SectionsdefMathlib.Data.Multiset.Sections, function or constant

Wording

the section of s (from the name)

English

Let $s$ be a multiset of the set of multisets of $x$. Then the section of $s$ is a multiset of the set of multisets of $x$.

Mathlib.Data.Multiset.Sort

Multiset.sortdefMathlib.Data.Multiset.Sort, function or constant

Wording

the sort of s and r (from the name)

English

Let $s$ be a multiset of $x$. Let $r$ be an element of $\mathrm{autoParam}$ applied to the set of functions from elements of $x$ and elements of $x$ to propositions and $\mathrm{Multiset\_\_sort\_\_\_auto\_1}$. Then the sort of $s$ and $r$ is a list of elements of $x$.

Mathlib.Data.Multiset.Sum

Multiset.disjSumdefMathlib.Data.Multiset.Sum, function or constant

Wording

no wording

English

Let $s$ be a multiset of $x$. Let $t$ be a multiset of $x_{1}$. Then $\operatorname{disjSum}$ applied to $s$ and $t$ is a multiset of $\mathrm{Sum}$ applied to $x$ and $x_{1}$ defined as the sum of the map of $\operatorname{inl}$ and $s$ and the map of $\operatorname{inr}$ and $t$.

Mathlib.Data.Multiset.Sym

Multiset.sym2defMathlib.Data.Multiset.Sym, function or constant

Wording

the symmetric power of m (from the name)

English

Let $m$ be a multiset of $x$. Then the symmetric power of $m$ is a multiset of the set of symmetric squares of $x$.

Mathlib.Data.Multiset.UnionInter

Multiset.interdefMathlib.Data.Multiset.UnionInter, function or constant

Wording

the intersection of s and t (from the name)

English

Let $s$ and $t$ be multisets of $x$. Then the intersection of $s$ and $t$ is a multiset of $x$.

Multiset.uniondefMathlib.Data.Multiset.UnionInter, function or constant

Wording

the union of s and t (from the name)

English

Let $s$ and $t$ be multisets of $x$. Then the union of $s$ and $t$ is a multiset of $x$ defined as $s - t + t$.

Mathlib.Data.Multiset.ZeroCons

Multiset.RelinductiveMathlib.Data.Multiset.ZeroCons, predicate

Wording

no wording

English

Let $r$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Let $x_{2}$ be a multiset of $x$. Let $x_{3}$ be a multiset of $x_{1}$. Then we can say that $\operatorname{Rel}$ holds for $r$, $x_{2}$ and $x_{3}$.

Multiset.Rel.belowinductiveMathlib.Data.Multiset.ZeroCons, predicate

Wording

no wording

English

Assume that $\operatorname{Rel}$ holds for $r$, $x_{2}$ and $x_{3}$. Then we can say that $\operatorname{below}$ holds for $t$.

Multiset.consdefMathlib.Data.Multiset.ZeroCons, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Let $s$ be a multiset of $x$. Then $\operatorname{cons}$ applied to $a$ and $s$ is a multiset of $x$.

Multiset.recOndefMathlib.Data.Multiset.ZeroCons, function or constant

Wording

no wording

English

Let $m$ be a multiset of $x$. Let $\mathrm{C\_0}$ be an element of $C$ applied to $0$. Let $\mathrm{C\_cons}$ be a function from elements $a_{1}$ of $x$ and multisets $m_{2}$ of $x$ and elements of $C$ applied to $m_{2}$ to elements of $C$ applied to $\operatorname{cons}$ applied to $a_{1}$ and $m_{2}$ such that for all elements $a$ and $\mathrm{a'}$ of $x$, for all multisets $m_{1}$ of $x$, for all elements $b$ of $C$ applied to $m_{1}$, $\mathrm{HEq}$ holds for $\mathrm{C\_cons}$ applied to $a$, $\operatorname{cons}$ applied to $\mathrm{a'}$ and $m_{1}$ and $\mathrm{C\_cons}$ applied to $\mathrm{a'}$, $m_{1}$ and $b$ and $\mathrm{C\_cons}$ applied to $\mathrm{a'}$, $\operatorname{cons}$ applied to $a$ and $m_{1}$ and $\mathrm{C\_cons}$ applied to $a$, $m_{1}$ and $b$. Then $\operatorname{recOn}$ applied to $m$, $\mathrm{C\_0}$, $a_{1}$, $m_{2}$, $\mathrm{C\_cons}$ and $\mathrm{C\_cons\_heq}$ is an element of $C$ applied to $m$.

Multiset.zerodefMathlib.Data.Multiset.ZeroCons, function or constant

Wording

the zero (from the name)

English

The zero is a multiset of $x$ defined as the multiset of $\operatorname{nil}$.

Mathlib.Data.NNRat.Defs

LibraryNote.specialised_high_priority_simp_lemmadefMathlib.Data.NNRat.Defs, function or constant

Wording

no wording

English

$\mathrm{LibraryNote\_\_specialised\_high\_priority\_simp\_lemma}$ is an element of $\operatorname{LibraryNote}$ defined as $\operatorname{default}$.

NNRat.coeHomdefMathlib.Data.NNRat.Defs, function or constant

Wording

the coercion homomorphism (from the name)

English

The coercion homomorphism is a ring homomorphism of the set of nonnegative rational numbers and $\Rational$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{cast}$ and $\mathrm{NNRat\_\_coe\_one}$ and $\mathrm{NNRat\_\_coe\_mul}$, $\mathrm{NNRat\_\_coe\_zero}$ and $\mathrm{NNRat\_\_coe\_add}$.

NNRat.divNatdefMathlib.Data.NNRat.Defs, function or constant

Wording

the quotient natural number of n and d (from the name)

English

Let $n$ and $d$ be natural numbers. Then the quotient natural number of $n$ and $d$ is a nonnegative rational number defined as $\operatorname{divInt}$ applied to $n$ and $d$.

NNRat.gidefMathlib.Data.NNRat.Defs, function or constant

Wording

no wording

English

$\operatorname{gi}$ is a Galois insertion of $\operatorname{toNNRat}$ and $\operatorname{cast}$ defined as the monotone intro of $\mathrm{Rat\_\_le\_coe\_toNNRat}$ and $\mathrm{NNRat\_\_toNNRat\_coe}$.

NNRat.numDenCasesOndefMathlib.Data.NNRat.Defs, function or constant

Wording

no wording

English

Let $q$ be a nonnegative rational number. Let $H$ be a function from natural numbers $n$ and natural numbers $d$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Neq} (d , 0)$ and elements of $\mathrm{Proof}$ applied to $\NatCoprimeMACRoC {n}{d}$ to elements of $C$ applied to the quotient natural number of $n$ and $d$. Then $\operatorname{numDenCasesOn}$ applied to $q$, $n$, $d$ and $H$ is an element of $C$ applied to $q$.

Rat.nnabsdefMathlib.Data.NNRat.Defs, function or constant

Wording

no wording

English

Let $x$ be a rational number. Then $\operatorname{nnabs}$ applied to $x$ is a nonnegative rational number defined as the absolute value of $x$.

Rat.toNNRatdefMathlib.Data.NNRat.Defs, function or constant

Wording

the nonnegative rational number of q (from the name)

English

Let $q$ be a rational number. Then the nonnegative rational number of $q$ is a nonnegative rational number defined as $\MaxmaxMACRoAF {q}{0}$.

Mathlib.Data.Nat.BinaryRec

Nat.binaryRecdefMathlib.Data.Nat.BinaryRec, function or constant

Wording

no wording

English

Let $\mathrm{zero}$ be an element of $\mathrm{motive}$ applied to $0$. Let $\mathrm{bit}$ be a function from elements $b$ of $\mathrm{Bool}$ and natural numbers $n_{1}$ and elements of $\mathrm{motive}$ applied to $n_{1}$ to elements of $\mathrm{motive}$ applied to the bit of $b$ and $n_{1}$. Let $n$ be a natural number. Then $\operatorname{binaryRec}$ applied to $\mathrm{zero}$, $b$, $n_{1}$, $\mathrm{bit}$ and $n$ is an element of $\mathrm{motive}$ applied to $n$.

Nat.binaryRec'defMathlib.Data.Nat.BinaryRec, function or constant

Wording

no wording

English

Let $\mathrm{zero}$ be an element of $\mathrm{motive}$ applied to $0$. Let $\mathrm{bit}$ be a function from elements $b$ of $\mathrm{Bool}$ and natural numbers $n_{1}$ and elements of $\mathrm{Proof}$ applied to the proposition that if $n_{1} = 0$, then $\EqtMACRoH {b}{\operatorname{true}}$ and elements of $\mathrm{motive}$ applied to $n_{1}$ to elements of $\mathrm{motive}$ applied to the bit of $b$ and $n_{1}$. Let $n$ be a natural number. Then $\operatorname{binaryRec'}$ applied to $\mathrm{zero}$, $b$, $n_{1}$, $\mathrm{bit}$ and $n$ is an element of $\mathrm{motive}$ applied to $n$.

Nat.binaryRecFromOnedefMathlib.Data.Nat.BinaryRec, function or constant

Wording

no wording

English

Let $\mathrm{zero}$ be an element of $\mathrm{motive}$ applied to $0$. Let $\mathrm{one}$ be an element of $\mathrm{motive}$ applied to $1$. Let $\mathrm{bit}$ be a function from elements $b$ of $\mathrm{Bool}$ and natural numbers $n_{1}$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Neq} (n_{1} , 0)$ and elements of $\mathrm{motive}$ applied to $n_{1}$ to elements of $\mathrm{motive}$ applied to the bit of $b$ and $n_{1}$. Let $n$ be a natural number. Then $\operatorname{binaryRecFromOne}$ applied to $\mathrm{zero}$, $\mathrm{one}$, $b$, $n_{1}$, $\mathrm{bit}$ and $n$ is an element of $\mathrm{motive}$ applied to $n$.

Nat.bitdefMathlib.Data.Nat.BinaryRec, function or constant

Wording

the bit of b and n (from the name)

English

Let $b$ be an element of $\mathrm{Bool}$. Let $n$ be a natural number. Then the bit of $b$ and $n$ is a natural number defined as $\mathrm{cond}$ applied to $b$, $2 \times n + 1$ and $2 \times n$.

Nat.bitCasesOndefMathlib.Data.Nat.BinaryRec, function or constant

Wording

no wording

English

Let $n$ be a natural number. Let $\mathrm{bit}$ be a function from elements $b$ of $\mathrm{Bool}$ and natural numbers $n_{1}$ to elements of $\mathrm{motive}$ applied to the bit of $b$ and $n_{1}$. Then $\operatorname{bitCasesOn}$ applied to $n$, $b$, $n_{1}$ and $\mathrm{bit}$ is an element of $\mathrm{motive}$ applied to $n$.

Mathlib.Data.Nat.BitIndices

Nat.bitIndicesdefMathlib.Data.Nat.BitIndices, function or constant

Wording

the bit indice of n (from the name)

English

Let $n$ be a natural number. Then the bit indice of $n$ is a list of natural numbers.

Mathlib.Data.Nat.Bits

Nat.bitsdefMathlib.Data.Nat.Bits, function or constant

Wording

the bit of x (from the name)

English

Let $x$ be a natural number. Then the bit of $x$ is a list of elements of $\mathrm{Bool}$ defined as $\operatorname{binaryRec}$ applied to $\operatorname{nil}$, the function that maps $b$, $x_{1}$ and $\mathrm{IH}$ to $\operatorname{cons}$ applied to $b$ and $\mathrm{IH}$ and $x$.

Nat.bodddefMathlib.Data.Nat.Bits, function or constant

Wording

no wording

English

Let $n$ be a natural number. Then $\operatorname{bodd}$ applied to $n$ is an element of $\mathrm{Bool}$ defined as $\operatorname{testBit}$ applied to $n$ and $0$.

Nat.div2defMathlib.Data.Nat.Bits, function or constant

Wording

the quotient of n (from the name)

English

Let $n$ be a natural number. Then the quotient of $n$ is a natural number defined as $\frac{ n}{2}$.

Nat.ldiffdefMathlib.Data.Nat.Bits, function or constant

Wording

no wording

English

Let $x$ and $x_{1}$ be natural numbers. Then $\operatorname{ldiff}$ applied to $x$ and $x_{1}$ is a natural number defined as $\operatorname{bitwise}$ applied to the function that maps $a$ and $b$ to $\operatorname{and}$ applied to $a$ and $\operatorname{not}$ applied to $b$, $x$ and $x_{1}$.

Nat.shiftLeft'defMathlib.Data.Nat.Bits, function or constant

Wording

the left shift of m and x (from the name)

English

Let $b$ be an element of $\mathrm{Bool}$. Let $m$ and $x$ be natural numbers. Then the left shift of $m$ and $x$ is a natural number defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{Nat\_\_shiftLeft'\_\_\_f}$ applied to $b$ and $m$.

Nat.sizedefMathlib.Data.Nat.Bits, function or constant

Wording

no wording

English

Let $x$ be a natural number. Then $\operatorname{size}$ applied to $x$ is a natural number defined as $\operatorname{binaryRec}$ applied to $0$, the function that maps $x_{1}$ and $x_{2}$ to $\mathrm{succ}$ and $x$.

Mathlib.Data.Nat.Cast.Basic

Nat.castAddMonoidHomdefMathlib.Data.Nat.Cast.Basic, function or constant

Wording

the cast additive monoid homomorphism of x (from the name)

English

Let $x$ be a set. Then the cast additive monoid homomorphism of $x$ is an additive monoid homomorphism of $\Natural$ and $x$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{toNatCast}$ and $\mathrm{Nat\_\_cast\_zero}$ and $\mathrm{Nat\_\_cast\_add}$.

Nat.castRingHomdefMathlib.Data.Nat.Cast.Basic, function or constant

Wording

the cast ring homomorphism of x (from the name)

English

Let $x$ be a set. Then the cast ring homomorphism of $x$ is a ring homomorphism of $\Natural$ and $x$.

Mathlib.Data.Nat.Cast.Defs

AddCommMonoidWithOneclassMathlib.Data.Nat.Cast.Defs, predicate

Wording

R is a additive commutative monoid with one (from the name)

English

Let $R$ be a set. Then we can say that $R$ is an additive commutative monoid with one.

AddMonoidWithOneclassMathlib.Data.Nat.Cast.Defs, predicate

Wording

R is a additive monoid with one (from the name)

English

Let $R$ be a set. Then we can say that $R$ is an additive monoid with one.

Nat.binCastdefMathlib.Data.Nat.Cast.Defs, function or constant

Wording

no wording

English

Let $x_{3}$ be a natural number. Then $\operatorname{binCast}$ applied to $x_{3}$ is an element of $R$.

Nat.unaryCastdefMathlib.Data.Nat.Cast.Defs, function or constant

Wording

the unary cast of x3 (from the name)

English

Let $x_{3}$ be a natural number. Then the unary cast of $x_{3}$ is an element of $R$ defined as $\operatorname{brecOn}$ applied to $x_{3}$ and $\mathrm{Nat\_\_unaryCast\_\_\_f}$.

Mathlib.Data.Nat.Cast.Order.Basic

Nat.castOrderEmbeddingdefMathlib.Data.Nat.Cast.Order.Basic, function or constant

Wording

the cast order embedding (from the name)

English

The cast order embedding is an order embedding of $\Natural$ and $x$ defined as the order embedding of $\operatorname{toNatCast}$ and $\mathrm{Nat\_\_strictMono\_cast}$.

Mathlib.Data.Nat.ChineseRemainder

Nat.chineseRemainderOfFinsetdefMathlib.Data.Nat.ChineseRemainder, function or constant

Wording

no wording

English

Let $a$ and $s$ be functions from elements of $x$ to natural numbers. Let $t$ be a finite set of $x$ such that for all elements $i_{1}$ of $x$, if $i_{1}$ is an element of $t$, then $s (i_{1})\neq 0$ and $\operatorname{Pairwise}$ holds for $t$ and $\operatorname{onFun}$ applied to $\NatCoprimeMACRoC$ and $s$. Then $\operatorname{chineseRemainderOfFinset}$ applied to $a$, $s$, $t$, $\mathrm{hs}$ and $\mathrm{pp}$ is an element of $\SubtypeSet {k}{\mathrm{forall} (x , \lambda i . \mathrm{if} (\MembershipmemMACRoT {t}{i}, \operatorname{ModEq} (s (i), k , a (i))))}$.

Nat.chineseRemainderOfListdefMathlib.Data.Nat.ChineseRemainder, function or constant

Wording

no wording

English

Let $a$ and $s$ be functions from elements of $x$ to natural numbers. Let $l$ be a list of elements of $x$ such that $\operatorname{Pairwise}$ holds for $\operatorname{onFun}$ applied to $\NatCoprimeMACRoC$ and $s$ and $l$. Then $\operatorname{chineseRemainderOfList}$ applied to $a$, $s$, $l$ and $h$ is an element of $\SubtypeSet {k}{\mathrm{forall} (x , \lambda i . \mathrm{if} (\MembershipmemMACRoT {l}{i}, \operatorname{ModEq} (s (i), k , a (i))))}$ defined as $\operatorname{brecOn}$ applied to $l$, $\mathrm{Nat\_\_chineseRemainderOfList\_\_\_f}$ applied to $a$ and $s$ and $h$.

Nat.chineseRemainderOfMultisetdefMathlib.Data.Nat.ChineseRemainder, function or constant

Wording

no wording

English

Let $a$ and $s$ be functions from elements of $x$ to natural numbers. Assume that $\operatorname{Nodup}$ holds for $m$. Assume that for all elements $i_{1}$ of $x$, if $i_{1}$ is an element of $m$, then $s (i_{1})\neq 0$. Assume that $\operatorname{Pairwise}$ holds for $\operatorname{ofPred}$ applied to the function that maps $x_{1}$ to $\MembershipmemMACRoT {m}{x_{1}}$ and $\operatorname{onFun}$ applied to $\NatCoprimeMACRoC$ and $s$. Then $\operatorname{chineseRemainderOfMultiset}$ applied to $a$, $s$, $h$, $h_{1}$ and $h_{2}$ is an element of $\SubtypeSet {k}{\mathrm{forall} (x , \lambda i . \mathrm{if} (\MembershipmemMACRoT {m}{i}, \operatorname{ModEq} (s (i), k , a (i))))}$.

Mathlib.Data.Nat.Choose.Basic

Nat.choosedefMathlib.Data.Nat.Choose.Basic, function or constant

Wording

no wording

English

Let $x$ and $x_{1}$ be natural numbers. Then $\operatorname{choose}$ applied to $x$ and $x_{1}$ is a natural number defined as $\operatorname{brecOn}$ applied to $x$, $\mathrm{Nat\_\_choose\_\_\_f}$ and $x_{1}$.

Nat.fast_choosedefMathlib.Data.Nat.Choose.Basic, function or constant

Wording

no wording

English

Let $n$ and $k$ be natural numbers. Then $\mathrm{Nat\_\_fast\_choose}$ applied to $n$ and $k$ is a natural number defined as $\frac{ \NatdescFactorialMACRoE {n}{k}}{k !}$.

Nat.multichoosedefMathlib.Data.Nat.Choose.Basic, function or constant

Wording

the multichoose of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be natural numbers. Then the multichoose of $x$ and $x_{1}$ is a natural number defined as $\mathrm{Nat\_\_multichoose\_\_\_unary}$ applied to $\operatorname{mk}$ applied to $x$ and $x_{1}$.

Mathlib.Data.Nat.Choose.Central

Nat.centralBinomdefMathlib.Data.Nat.Choose.Central, function or constant

Wording

the central binom of n (from the name)

English

Let $n$ be a natural number. Then the central binom of $n$ is a natural number defined as $\operatorname{choose}$ applied to $2 \times n$ and $n$.

Mathlib.Data.Nat.Choose.Multinomial

Finsupp.multinomialdefMathlib.Data.Nat.Choose.Multinomial, function or constant

Wording

no wording

English

Let $f$ be an element of $\FinsuppMACRoQ {x}{\Natural}$. Then $\operatorname{multinomial}$ applied to $f$ is a natural number defined as the quotient of the factorial of the sum of $f$ and the function that maps $x_{1}$ to $\mathrm{id}$ and $\FinsuppProd {f}{x_{2}}{n}{(n !)}$.

List.multinomialdefMathlib.Data.Nat.Choose.Multinomial, function or constant

Wording

no wording

English

Let $l$ be a list of natural numbers. Then $\operatorname{multinomial}$ applied to $l$ is a natural number defined as $\operatorname{multinomial}$ applied to the finitely supported function of $l$.

Multiset.countPermsdefMathlib.Data.Nat.Choose.Multinomial, function or constant

Wording

no wording

English

Let $m$ be a multiset of $x$. Then $\operatorname{countPerms}$ applied to $m$ is a natural number defined as $\operatorname{multinomial}$ applied to $\operatorname{toFinsupp}$ applied to $m$.

Multiset.evalMultinomialdefMathlib.Data.Nat.Choose.Multinomial, function or constant

Wording

no wording

English

$\operatorname{evalMultinomial}$ is an element of $\operatorname{PositivityExt}$.

Multiset.multinomialdefMathlib.Data.Nat.Choose.Multinomial, function or constant

Wording

no wording

English

Let $m$ be a multiset of $\Natural$. Then $\operatorname{multinomial}$ applied to $m$ is a natural number.

Nat.multinomialdefMathlib.Data.Nat.Choose.Multinomial, function or constant

Wording

the multinomial coefficient of s and f (from the docstring)

English

Let $s$ be a finite set of $x$. Let $f$ be a function from elements of $x$ to natural numbers. Then the multinomial coefficient of $s$ and $f$ is a natural number defined as $\frac{ (\FinsetSum {s}{i}{f (i)})!}{\FinsetProd {s}{i_{1}}{(f (i_{1})!)}}$.

Mathlib.Data.Nat.Count

Nat.countdefMathlib.Data.Nat.Count, function or constant

Wording

the count of p and n (from the name)

English

Let $p$ be a function from natural numbers to propositions. Let $n$ be a natural number. Then the count of $p$ and $n$ is a natural number defined as $\operatorname{countP}$ applied to the function that maps $b$ to $\operatorname{decide}$ applied to $p$ applied to $b$ and $\operatorname{range}$ applied to $n$.

Mathlib.Data.Nat.Digits.Defs

Nat.digitsdefMathlib.Data.Nat.Digits.Defs, function or constant

Wording

the digit of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be natural numbers. Then the digit of $x$ and $x_{1}$ is a list of natural numbers.

Nat.digitsAux0defMathlib.Data.Nat.Digits.Defs, function or constant

Wording

the digit of x (from the name)

English

Let $x$ be a natural number. Then the digit of $x$ is a list of natural numbers.

Nat.digitsAux1defMathlib.Data.Nat.Digits.Defs, function or constant

Wording

the digit of n (from the name)

English

Let $n$ be a natural number. Then the digit of $n$ is a list of natural numbers defined as $\operatorname{replicate}$ applied to $n$ and $1$.

Nat.ofDigitsdefMathlib.Data.Nat.Digits.Defs, function or constant

Wording

the natural number of b and x2 (from the name)

English

Let $b$ be an element of $x$. Let $x_{2}$ be a list of natural numbers. Then the natural number of $b$ and $x_{2}$ is an element of $x$ defined as $\operatorname{brecOn}$ applied to $x_{2}$ and $\mathrm{Nat\_\_ofDigits\_\_\_f}$ applied to $b$.

Mathlib.Data.Nat.Digits.Lemmas

List.consFixedLengthDigitsdefMathlib.Data.Nat.Digits.Lemmas, function or constant

Wording

no wording

English

Assume that $1 < b$. Let $l$ and $d$ be natural numbers. Then $\operatorname{consFixedLengthDigits}$ applied to $\mathrm{hb}$, $l$ and $d$ is a finite set of the set of lists of natural numbers defined as the forward image of the fixed length digit of $\mathrm{hb}$ and $l$ under the function that maps $L$ to $\operatorname{cons}$ applied to $d$ and $L$.

List.fixedLengthDigitsdefMathlib.Data.Nat.Digits.Lemmas, function or constant

Wording

the fixed length digit of hb and l (from the name)

English

Assume that $1 < b$. Let $l$ be a natural number. Then the fixed length digit of $\mathrm{hb}$ and $l$ is a finite set of the set of lists of natural numbers defined as the finite set of $\operatorname{ofPred}$ applied to the function that maps $L$ to the proposition that $\operatorname{length} (L)= l$ and for all natural numbers $x$, if $x$ is an element of $L$, then $x < b$.

Nat.digitsAppenddefMathlib.Data.Nat.Digits.Lemmas, function or constant

Wording

no wording

English

Let $b$, $l$ and $n$ be natural numbers. Then $\operatorname{digitsAppend}$ applied to $b$, $l$ and $n$ is a list of natural numbers defined as $\operatorname{hAppend}$ applied to the digit of $b$ and $n$ and $\operatorname{replicate}$ applied to the difference between $l$ and $\operatorname{length}$ applied to the digit of $b$ and $n$ and $0$.

Mathlib.Data.Nat.Dist

Nat.distdefMathlib.Data.Nat.Dist, function or constant

Wording

the distance of n and m (from the name)

English

Let $n$ and $m$ be natural numbers. Then the distance of $n$ and $m$ is a natural number defined as $n - m + (m - n)$.

Mathlib.Data.Nat.DvdSequence

IsDvdSequencedefMathlib.Data.Nat.DvdSequence, predicate

Wording

f is a divisibility sequence (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $f$ is a divisibility sequence, if for all elements $a$ and $b$ of $x$, if $a$ divides $b$, then $\divides {f (a)}{f (b)}$.

Nat.IsStrongDvdSequencedefMathlib.Data.Nat.DvdSequence, predicate

Wording

f is a strong divisibility sequence (from the name)

English

Let $f$ be a function from natural numbers to natural numbers. Then $f$ is a strong divisibility sequence, if for all natural numbers $a$ and $b$, the greatest common divisor of $f$ applied to $a$ and $f$ applied to $b$ is equal to $f$ applied to the greatest common divisor of $a$ and $b$.

Mathlib.Data.Nat.EvenOddRec

Nat.evenOddRecdefMathlib.Data.Nat.EvenOddRec, function or constant

Wording

no wording

English

Let $h_{0}$ be an element of $P$ applied to $0$. Let $\mathrm{h\_even}$ be a function from natural numbers $n_{2}$ and elements of $P$ applied to $n_{2}$ to elements of $P$ applied to $2 \times n_{2}$. Let $\mathrm{h\_odd}$ be a function from natural numbers $n_{1}$ and elements of $P$ applied to $n_{1}$ to elements of $P$ applied to $2 \times n_{1} + 1$. Let $n$ be a natural number. Then $\operatorname{evenOddRec}$ applied to $h_{0}$, $n_{2}$, $\mathrm{h\_even}$, $n_{1}$, $\mathrm{h\_odd}$ and $n$ is an element of $P$ applied to $n$.

Nat.evenOddStrongRecdefMathlib.Data.Nat.EvenOddRec, function or constant

Wording

no wording

English

Let $\mathrm{h\_even}$ be a function from natural numbers $n_{2}$ and functions from natural numbers $k_{1}$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (k_{1} , 2 \times n_{2})$ to elements of $P$ applied to $k_{1}$ to elements of $P$ applied to $2 \times n_{2}$. Let $\mathrm{h\_odd}$ be a function from natural numbers $n_{1}$ and functions from natural numbers $k$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (k , 2 \times n_{1} + 1)$ to elements of $P$ applied to $k$ to elements of $P$ applied to $2 \times n_{1} + 1$. Let $n$ be a natural number. Then $\operatorname{evenOddStrongRec}$ applied to $n_{2}$, $\mathrm{h\_even}$, $n_{1}$, $\mathrm{h\_odd}$ and $n$ is an element of $P$ applied to $n$.

Mathlib.Data.Nat.Factorial.Basic

Nat.ascFactorialdefMathlib.Data.Nat.Factorial.Basic, function or constant

Wording

no wording

English

Let $n$ and $x$ be natural numbers. Then $\operatorname{ascFactorial}$ applied to $n$ and $x$ is a natural number defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{Nat\_\_ascFactorial\_\_\_f}$ applied to $n$.

Nat.ascFactorialBinarydefMathlib.Data.Nat.Factorial.Basic, function or constant

Wording

no wording

English

Let $n$ and $k$ be natural numbers. Then $\operatorname{ascFactorialBinary}$ applied to $n$ and $k$ is a natural number defined as $\mathrm{Nat\_\_ascFactorialBinary\_\_\_unary}$ applied to $\operatorname{mk}$ applied to $n$ and $k$.

Nat.descFactorialdefMathlib.Data.Nat.Factorial.Basic, function or constant

Wording

the descending factorial of n of order x (by hand)

English

Let $n$ and $x$ be natural numbers. Then $\NatdescFactorialMACRoE {n}{x}$ is a natural number defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{Nat\_\_descFactorial\_\_\_f}$ applied to $n$.

Nat.descFactorialBinarydefMathlib.Data.Nat.Factorial.Basic, function or constant

Wording

no wording

English

Let $n$ and $k$ be natural numbers. Then $\operatorname{descFactorialBinary}$ applied to $n$ and $k$ is a natural number defined as $\iteMACRoG {\mathrm{Lt} (n , k)}{0}{\operatorname{ascFactorialBinary} (n - k + 1 , k)}$.

Nat.factorialdefMathlib.Data.Nat.Factorial.Basic, function or constant

Wording

no wording

English

Let $x$ be a natural number. Then $\operatorname{factorial}$ applied to $x$ is a natural number defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{Nat\_\_factorial\_\_\_f}$.

Nat.factorialBinarySplittingdefMathlib.Data.Nat.Factorial.Basic, function or constant

Wording

the factorial binary splitting of n (from the name)

English

Let $n$ be a natural number. Then the factorial binary splitting of $n$ is a natural number defined as $\operatorname{ascFactorialBinary}$ applied to $1$ and $n$.

Mathlib.Data.Nat.Factorial.DoubleFactorial

Nat.doubleFactorialdefMathlib.Data.Nat.Factorial.DoubleFactorial, function or constant

Wording

the double factorial of x (from the docstring)

English

Let $x$ be a natural number. Then the double factorial of $x$ is a natural number defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{Nat\_\_doubleFactorial\_\_\_f}$.

Mathlib.Data.Nat.Factorial.SuperFactorial

Nat.superFactorialdefMathlib.Data.Nat.Factorial.SuperFactorial, function or constant

Wording

the super factorial of x (from the name)

English

Let $x$ be a natural number. Then the super factorial of $x$ is a natural number defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{Nat\_\_superFactorial\_\_\_f}$.

Mathlib.Data.Nat.Factorization.Defs

Nat.factorizationdefMathlib.Data.Nat.Factorization.Defs, function or constant

Wording

the factorization of n (by hand)

English

Let $n$ be a natural number. Then the factorization of $n$ is an element of $\FinsuppMACRoQ {\Natural}{\Natural}$ defined as $\operatorname{toFinsupp}$ applied to the multiset of the prime factorization of $n$.

Nat.factorizationEquivdefMathlib.Data.Nat.Factorization.Defs, function or constant

Wording

the factorization equivalence (from the name)

English

The factorization equivalence is an element of $\EquivMACRoAE {\PNatMACRoAD}{(\SubtypeSet {f}{\mathrm{forall} (\Natural , \lambda p . \mathrm{if} (\MembershipmemMACRoT {\FinsuppsupportMACRoR {f}}{p}, \mathrm{prime} (p)))})}$.

Nat.factorizationLCMLeftdefMathlib.Data.Nat.Factorization.Defs, function or constant

Wording

the left factorization least common multiple of a and b (from the name)

English

Let $a$ and $b$ be elements of $\Natural$. Then $\NatfactorizationLCMLeftMACRoV {a}{b}$ is an element of $\Natural$ defined as $\FinsuppProd {\operatorname{factorization} (\NatlcmMACRoX {a}{b})}{p}{n}{(\iteMACRoG {\mathrm{Leq} (\NatfactorizationappMACRoI {b}{p}, \NatfactorizationappMACRoI {a}{p})}{(p ^ {n})}{1})}$.

Nat.factorizationLCMRightdefMathlib.Data.Nat.Factorization.Defs, function or constant

Wording

the right factorization least common multiple of a and b (from the name)

English

Let $a$ and $b$ be elements of $\Natural$. Then $\NatfactorizationLCMRightMACRoW {a}{b}$ is an element of $\Natural$ defined as $\FinsuppProd {\operatorname{factorization} (\NatlcmMACRoX {a}{b})}{p}{n}{(\iteMACRoG {\mathrm{Leq} (\NatfactorizationappMACRoI {b}{p}, \NatfactorizationappMACRoI {a}{p})}{1}{(p ^ {n})})}$.

Mathlib.Data.Nat.Factorization.Induction

Nat.recOnMuldefMathlib.Data.Nat.Factorization.Induction, function or constant

Wording

no wording

English

Let $\mathrm{zero}$ be an element of $\mathrm{motive}$ applied to $0$. Let $\mathrm{one}$ be an element of $\mathrm{motive}$ applied to $1$. Let $\mathrm{prime}$ be a function from natural numbers $p$ and elements of $\mathrm{Proof}$ applied to the proposition that $p$ is prime to elements of $\mathrm{motive}$ applied to $p$. Let $\mathrm{mul}$ be a function from natural numbers $a_{1}$ and natural numbers $b$ and elements of $\mathrm{motive}$ applied to $a_{1}$ and elements of $\mathrm{motive}$ applied to $b$ to elements of $\mathrm{motive}$ applied to $a_{1} \times b$. Let $a$ be a natural number. Then $\operatorname{recOnMul}$ applied to $\mathrm{zero}$, $\mathrm{one}$, $p$, $\mathrm{prime}$, $a_{1}$, $b$, $\mathrm{mul}$ and $a$ is an element of $\mathrm{motive}$ applied to $a$.

Nat.recOnPosPrimePosCoprimedefMathlib.Data.Nat.Factorization.Induction, function or constant

Wording

no wording

English

Let $\mathrm{prime\_pow}$ be a function from natural numbers $p$ and natural numbers $n$ and elements of $\mathrm{Proof}$ applied to the proposition that $p$ is prime and elements of $\mathrm{Proof}$ applied to the proposition that $0$ is less than $n$ to elements of $\mathrm{motive}$ applied to $p ^ {n}$. Let $\mathrm{zero}$ be an element of $\mathrm{motive}$ applied to $0$. Let $\mathrm{one}$ be an element of $\mathrm{motive}$ applied to $1$. Let $\mathrm{coprime}$ be a function from natural numbers $a_{1}$ and natural numbers $b$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (1 , a_{1})$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (1 , b)$ and elements of $\mathrm{Proof}$ applied to $\NatCoprimeMACRoC {a_{1}}{b}$ and elements of $\mathrm{motive}$ applied to $a_{1}$ and elements of $\mathrm{motive}$ applied to $b$ to elements of $\mathrm{motive}$ applied to $a_{1} \times b$. Let $a$ be a natural number. Then $\operatorname{recOnPosPrimePosCoprime}$ applied to $p$, $n$, $\mathrm{prime\_pow}$, $\mathrm{zero}$, $\mathrm{one}$, $a_{1}$, $b$, $\mathrm{coprime}$ and $a$ is an element of $\mathrm{motive}$ applied to $a$.

Nat.recOnPrimeCoprimedefMathlib.Data.Nat.Factorization.Induction, function or constant

Wording

no wording

English

Let $\mathrm{zero}$ be an element of $\mathrm{motive}$ applied to $0$. Let $\mathrm{prime\_pow}$ be a function from elements $p$ of $\Natural$ and natural numbers $n$ and elements of $\mathrm{Proof}$ applied to the proposition that $p$ is prime to elements of $\mathrm{motive}$ applied to $p ^ {n}$. Let $\mathrm{coprime}$ be a function from natural numbers $a_{1}$ and natural numbers $b$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (1 , a_{1})$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (1 , b)$ and elements of $\mathrm{Proof}$ applied to $\NatCoprimeMACRoC {a_{1}}{b}$ and elements of $\mathrm{motive}$ applied to $a_{1}$ and elements of $\mathrm{motive}$ applied to $b$ to elements of $\mathrm{motive}$ applied to $a_{1} \times b$. Let $a$ be a natural number. Then $\operatorname{recOnPrimeCoprime}$ applied to $\mathrm{zero}$, $p$, $n$, $\mathrm{prime\_pow}$, $a_{1}$, $b$, $\mathrm{coprime}$ and $a$ is an element of $\mathrm{motive}$ applied to $a$ defined as the function that maps $a_{1}$, $b$, $\mathrm{coprime}$ and $a$ to $\operatorname{recOnPosPrimePosCoprime}$ applied to the function that maps $p$, $n$, $h$ and $h_{1}$ to $p$ applied to $p$, $n$ and $h$, $\mathrm{zero}$, $p$ applied to $2$, $0$ and $\mathrm{Nat\_\_prime\_two}$, $n$, $\mathrm{prime\_pow}$, $a_{1}$, $b$, $\mathrm{coprime}$ and $a$.

Nat.recOnPrimePowdefMathlib.Data.Nat.Factorization.Induction, function or constant

Wording

no wording

English

Let $\mathrm{zero}$ be an element of $\mathrm{motive}$ applied to $0$. Let $\mathrm{one}$ be an element of $\mathrm{motive}$ applied to $1$. Let $\mathrm{prime\_pow\_mul}$ be a function from natural numbers $a_{1}$ and natural numbers $p$ and natural numbers $n$ and elements of $\mathrm{Proof}$ applied to the proposition that $p$ is prime and elements of $\mathrm{Proof}$ applied to the proposition that $p$ does not divide $a_{1}$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (0 , n)$ and elements of $\mathrm{motive}$ applied to $a_{1}$ to elements of $\mathrm{motive}$ applied to $p ^ {n}\times a_{1}$. Let $a$ be a natural number. Then $\operatorname{recOnPrimePow}$ applied to $\mathrm{zero}$, $\mathrm{one}$, $a_{1}$, $p$, $n$, $\mathrm{prime\_pow\_mul}$ and $a$ is an element of $\mathrm{motive}$ applied to $a$.

Mathlib.Data.Nat.Factorization.PrimePow

Nat.Primes.prodNatEquivdefMathlib.Data.Nat.Factorization.PrimePow, function or constant

Wording

the product natural equivalence (from the name)

English

The product natural equivalence is an element of $\EquivMACRoAE {\mathrm{Prod} (\NatPrimesMACRoA , \Natural)}{(\SubtypeSet {n}{\mathrm{IsPrimePow} (n)})}$.

Mathlib.Data.Nat.Factorization.Root

Nat.ceilRootdefMathlib.Data.Nat.Factorization.Root, function or constant

Wording

the ceiling root of a of order n (by hand)

English

Let $n$ and $a$ be elements of $\Natural$. Then $\NatceilRootMACRoK {n}{a}$ is an element of $\Natural$ defined as $\iteMACRoG {\mathrm{or} (\mathrm{Eq} (n , 0), \mathrm{Eq} (a , 0))}{0}{(\FinsuppProd {\operatorname{factorization} (a)}{p}{k}{(p ^ {\frac{ k + n - 1}{n}})})}$.

Nat.floorRootdefMathlib.Data.Nat.Factorization.Root, function or constant

Wording

the floor root of a of order n (by hand)

English

Let $n$ and $a$ be elements of $\Natural$. Then $\NatfloorRootMACRoJ {n}{a}$ is an element of $\Natural$ defined as $\iteMACRoG {\mathrm{or} (\mathrm{Eq} (n , 0), \mathrm{Eq} (a , 0))}{0}{(\FinsuppProd {\operatorname{factorization} (a)}{p}{k}{(p ^ {\frac{ k}{n}})})}$.

Mathlib.Data.Nat.Factors

Nat.primeFactorsListdefMathlib.Data.Nat.Factors, function or constant

Wording

the prime factorization of x (by hand)

English

Let $x$ be a natural number. Then the prime factorization of $x$ is a list of natural numbers.

Mathlib.Data.Nat.Fib.Basic

Nat.fastFibdefMathlib.Data.Nat.Fib.Basic, function or constant

Wording

no wording

English

Let $n$ be a natural number. Then $\operatorname{fastFib}$ applied to $n$ is a natural number defined as $\ProdfstMACRoZ {\operatorname{fastFibAux} (n)}$.

Mathlib.Data.Nat.Fib.Zeckendorf

List.IsZeckendorfRepdefMathlib.Data.Nat.Fib.Zeckendorf, predicate

Wording

l is a Zeckendorf representation (from the name)

English

Let $l$ be a list of natural numbers. Then $l$ is a Zeckendorf representation, if $\operatorname{IsChain}$ holds for the function that maps $a$ and $b$ to $\mathrm{Leq} (b + 2 , a)$ and $\operatorname{hAppend}$ applied to $l$ and $\operatorname{cons}$ applied to $0$ and $\operatorname{nil}$.

Nat.greatestFibdefMathlib.Data.Nat.Fib.Zeckendorf, function or constant

Wording

the greatest index of n (from the docstring)

English

Let $n$ be a natural number. Then the greatest index of $n$ is a natural number defined as $\operatorname{findGreatest}$ applied to the function that maps $k$ to $\mathrm{Leq} (\operatorname{fib} (k), n)$ and $n + 1$.

Nat.zeckendorfdefMathlib.Data.Nat.Fib.Zeckendorf, function or constant

Wording

the Zeckendorf representation of x (from the docstring)

English

Let $x$ be a natural number. Then the Zeckendorf representation of $x$ is a list of natural numbers.

Nat.zeckendorfEquivdefMathlib.Data.Nat.Fib.Zeckendorf, function or constant

Wording

the Zeckendorf equivalence (from the name)

English

The Zeckendorf equivalence is an element of $\EquivMACRoAE {\Natural}{(\SubtypeSet {l}{\operatorname{IsZeckendorfRep} (l)})}$.

Mathlib.Data.Nat.Find

Nat.finddefMathlib.Data.Nat.Find, function or constant

Wording

no wording

English

Assume that there exists a natural number $n$, such that $p$ holds for $n$. Then $\operatorname{find}$ applied to $H$ is a natural number defined as $\operatorname{findX}$ applied to $H$.

Nat.findGreatestdefMathlib.Data.Nat.Find, function or constant

Wording

no wording

English

Let $P$ be a function from natural numbers to propositions. Let $x_{1}$ be a natural number. Then $\operatorname{findGreatest}$ applied to $P$ and $x_{1}$ is a natural number defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{Nat\_\_findGreatest\_\_\_f}$ applied to $P$.

Nat.findXdefMathlib.Data.Nat.Find, function or constant

Wording

no wording

English

Assume that there exists a natural number $n_{1}$, such that $p$ holds for $n_{1}$. Then $\operatorname{findX}$ applied to $H$ is an element of $\SubtypeSet {n}{\mathrm{and} (p (n), \mathrm{forall} (\Natural , \lambda m . \mathrm{if} (\mathrm{Lt} (m , n), \mathrm{not} (p (m)))))}$.

Mathlib.Data.Nat.Init

LibraryNote.foundational_algebra_order_theorydefMathlib.Data.Nat.Init, function or constant

Wording

the foundational algebra order theory (from the name)

English

The foundational algebra order theory is an element of $\operatorname{LibraryNote}$ defined as $\operatorname{default}$.

Nat.AtLeastTwoclassMathlib.Data.Nat.Init, predicate

Wording

no wording

English

Let $n$ be a natural number. Then we can say that $\operatorname{AtLeastTwo}$ holds for $n$.

Nat.decreasingInductiondefMathlib.Data.Nat.Init, function or constant

Wording

the decreasing induction of of_succ and k (from the name)

English

Let $\mathrm{of\_succ}$ be a function from natural numbers $k$ and elements $h$ of $\mathrm{Proof}$ applied to $\mathrm{Lt} (k , n)$ and elements of $\mathrm{motive}$ applied to $k + 1$ and $h$ to elements of $\mathrm{motive}$ applied to $k$ and $\mathrm{Nat\_\_le\_of\_succ\_le}$ applied to $h$. Let $\mathrm{self}$ be an element of $\mathrm{motive}$ applied to $n$ and $\mathrm{Nat\_\_le\_refl}$ applied to $n$. Assume that $m \leq n$. Then the decreasing induction of $k$ and $h$ is an element of $\mathrm{motive}$ applied to $m$ and $\mathrm{mn}$.

Nat.decreasingInduction'defMathlib.Data.Nat.Init, function or constant

Wording

the decreasing induction of h and mn (from the name)

English

Let $h$ be a function from natural numbers $k$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (k , n)$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (m , k)$ and elements of $P$ applied to $k + 1$ to elements of $P$ applied to $k$. Assume that $m \leq n$. Let $\mathrm{hP}$ be an element of $P$ applied to $n$. Then the decreasing induction of $k$ and $\mathrm{mn}$ is an element of $P$ applied to $m$ defined as the function that maps $\mathrm{hP}$ to the decreasing induction of the function that maps $k$, $\mathrm{hk}$, $\mathrm{ih}$ and $h_{1}$ to $h_{1}$ applied to $k$, $\mathrm{Nat\_\_lt\_of\_succ\_le}$ applied to $\mathrm{hk}$, $\mathrm{Nat\_\_le\_refl}$ applied to $k$ and $\mathrm{ih}$ applied to the function that maps $\mathrm{k'}$, $\mathrm{hk'}$ and $\mathrm{h''}$ to $h_{1}$ applied to $\mathrm{k'}$, $\mathrm{hk'}$ and $\mathrm{Nat\_\_le\_of\_succ\_le}$ applied to $\mathrm{h''}$ and the function that maps $h_{2}$ to $\mathrm{mn}$.

Nat.leRecdefMathlib.Data.Nat.Init, function or constant

Wording

no wording

English

Let $\mathrm{refl}$ be an element of $\mathrm{motive}$ applied to $n$ and $\mathrm{Nat\_\_le\_refl}$ applied to $n$. Let $\mathrm{le\_succ\_of\_le}$ be a function from natural numbers $k$ and elements $h_{1}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (n , k)$ and elements of $\mathrm{motive}$ applied to $k$ and $h_{1}$ to elements of $\mathrm{motive}$ applied to $k + 1$ and $\mathrm{Nat\_\_le\_succ\_of\_le}$ applied to $h_{1}$. Assume that $n \leq m$. Then $\operatorname{leRec}$ applied to $\mathrm{refl}$, $k$, $h_{1}$, $\mathrm{le\_succ\_of\_le}$ and $h$ is an element of $\mathrm{motive}$ applied to $m$ and $h$ defined as the function that maps $\mathrm{le\_succ\_of\_le}$ and $h$ to $\operatorname{brecOn}$ applied to $m$, $\mathrm{Nat\_\_leRec\_\_\_f}$ applied to $\mathrm{refl}$ and $k$, $h_{1}$, $\mathrm{le\_succ\_of\_le}$ and $h$.

Nat.leRecOndefMathlib.Data.Nat.Init, function or constant

Wording

no wording

English

Assume that $n \leq m$. Let $x$ be a function from natural numbers $k$ and elements of $C$ applied to $k$ to elements of $C$ applied to $k + 1$. Let $x_{1}$ be an element of $C$ applied to $n$. Then $\operatorname{leRecOn}$ applied to $h$, $k$, $x$ and $x_{1}$ is an element of $C$ applied to $m$ defined as the function that maps $x_{1}$ to $\operatorname{leRec}$ applied to $x$, the function that maps $x_{2}$ and $h_{1}$ to $k$ applied to $x_{2}$, $h$ and $x_{1}$.

Nat.pincerRecursiondefMathlib.Data.Nat.Init, function or constant

Wording

the pincer recursion of n1 and H (from the name)

English

Let $\mathrm{Ha0}$ be a function from natural numbers $m_{1}$ to elements of $P$ applied to $m_{1}$ and $0$. Let $\mathrm{H0b}$ be a function from natural numbers $n_{1}$ to elements of $P$ applied to $0$ and $n_{1}$. Let $H$ be a function from natural numbers $x$ and natural numbers $y$ and elements of $P$ applied to $x$ and the successor of $y$ and elements of $P$ applied to the successor of $x$ and $y$ to elements of $P$ applied to the successor of $x$ and the successor of $y$. Let $n$ and $m$ be natural numbers. Then the pincer recursion of $\mathrm{H0b}$ and $x$ is an element of $P$ applied to $n$ and $m$ defined as the function that maps $y$, $H$, $n$ and $m$ to $\mathrm{Nat\_\_pincerRecursion\_\_\_unary}$ applied to $m_{1}$, $\mathrm{Ha0}$, $n_{1}$, $\operatorname{mk}$ applied to $\mathrm{H0b}$ and $x$, $y$, $H$, $n$ and $m$.

Nat.stepInductiondefMathlib.Data.Nat.Init, function or constant

Wording

the step induction of i1 and step (from the name)

English

Let $k$ and $a$ be natural numbers. Let $\mathrm{base}$ be a function from elements $i_{1}$ of $\Natural$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (i_{1} , k)$ to elements of $\mathrm{motive}$ applied to $i_{1}$. Let $\mathrm{step}$ be a function from natural numbers $n$ and functions from natural numbers $i$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (i , k)$ to elements of $\mathrm{motive}$ applied to $n + i$ to elements of $\mathrm{motive}$ applied to $n + k$. Then the step induction of $\mathrm{base}$ and $n$ is an element of $\mathrm{motive}$ applied to $a$.

Nat.strongSubRecursiondefMathlib.Data.Nat.Init, function or constant

Wording

the strong difference recursion of m1 and n1 (from the name)

English

Let $H$ be a function from natural numbers $m_{1}$ and natural numbers $n_{1}$ and functions from natural numbers $x_{1}$ and natural numbers $y$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (x_{1} , m_{1})$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (y , n_{1})$ to elements of $P$ applied to $x_{1}$ and $y$ to elements of $P$ applied to $m_{1}$ and $n_{1}$. Let $n$ and $m$ be natural numbers. Then the strong difference recursion of $n_{1}$ and $H$ is an element of $P$ applied to $n$ and $m$ defined as the function that maps $n$ and $m$ to $\mathrm{Nat\_\_strongSubRecursion\_\_\_unary}$ applied to $m_{1}$, $\operatorname{mk}$ applied to $n_{1}$ and $H$, $n$ and $m$.

Nat.twoStepInductiondefMathlib.Data.Nat.Init, function or constant

Wording

no wording

English

Let $\mathrm{zero}$ be an element of $\mathrm{motive}$ applied to $0$. Let $\mathrm{one}$ be an element of $\mathrm{motive}$ applied to $1$. Let $\mathrm{more}$ be a function from natural numbers $n$ and elements of $\mathrm{motive}$ applied to $n$ and elements of $\mathrm{motive}$ applied to $n + 1$ to elements of $\mathrm{motive}$ applied to $n + 2$. Let $a$ be a natural number. Then $\operatorname{twoStepInduction}$ applied to $\mathrm{zero}$, $\mathrm{one}$, $n$, $\mathrm{more}$ and $a$ is an element of $\mathrm{motive}$ applied to $a$ defined as the function that maps $a$ to $\operatorname{brecOn}$ applied to $\mathrm{more}$, $\mathrm{Nat\_\_twoStepInduction\_\_\_f}$ applied to $\mathrm{zero}$, $\mathrm{one}$ and $n$ and $a$.

Mathlib.Data.Nat.Log

Nat.clogdefMathlib.Data.Nat.Log, function or constant

Wording

no wording

English

Let $b$ and $n$ be natural numbers. Then $\operatorname{clog}$ applied to $b$ and $n$ is a natural number defined as $\iteMACRoG {\mathrm{and} (\mathrm{Lt} (1 , b), \mathrm{Lt} (1 , n))}{(\ProdsndMACRoAA {\operatorname{go} (n , b , n)}+ 1)}{0}$.

Nat.logdefMathlib.Data.Nat.Log, function or constant

Wording

the logarithm of b and n (from the name)

English

Let $b$ and $n$ be natural numbers. Then the logarithm of $b$ and $n$ is a natural number defined as $\iteMACRoG {\mathrm{Leq} (b , 1)}{0}{\ProdsndMACRoAA {\operatorname{go} (n , b , n)}}$.

Mathlib.Data.Nat.MaxPowDiv

Nat.divMaxPowdefMathlib.Data.Nat.MaxPowDiv, function or constant

Wording

the quotient maximum power of n and p (from the name)

English

Let $n$ and $p$ be natural numbers. Then the quotient maximum power of $n$ and $p$ is a natural number defined as the second element of the maximum power divisibility quotient of $p$ and $n$.

Nat.maxPowDvdDivdefMathlib.Data.Nat.MaxPowDiv, function or constant

Wording

the maximum power divisibility quotient of p and n (from the name)

English

Let $p$ and $n$ be natural numbers. Then the maximum power divisibility quotient of $p$ and $n$ is an element of $\mathrm{Prod}$ applied to $\Natural$ and $\Natural$ defined as $\mathrm{dite}$ applied to the proposition that $1 < p$ and $n \neq 0$, the function that maps $H$ to $\operatorname{go}$ applied to $n$, $p$ and $H$ and the function that maps $H_{1}$ to $\ProdmkMACRoU {0}{n}$.

Mathlib.Data.Nat.MaxPrimeFac

Nat.maxPrimeFacdefMathlib.Data.Nat.MaxPrimeFac, function or constant

Wording

the greatest prime divisor of n (from the docstring)

English

Let $n$ be a natural number. Then the greatest prime divisor of $n$ is a natural number defined as $\operatorname{getLastD}$ applied to the prime factorization of $n$ and $n$.

Mathlib.Data.Nat.ModEq

Nat.ModEqdefMathlib.Data.Nat.ModEq, predicate

Wording

no wording

English

Let $n$, $a$ and $b$ be natural numbers. Then $\operatorname{ModEq}$ holds for $n$, $a$ and $b$, if $\HModhModMACRoF {a}{n}= \HModhModMACRoF {b}{n}$.

Nat.chineseRemainderdefMathlib.Data.Nat.ModEq, function or constant

Wording

no wording

English

Assume that $n$ and $m$ are coprime. Let $a$ and $b$ be natural numbers. Then $\operatorname{chineseRemainder}$ applied to $\mathrm{co}$, $a$ and $b$ is an element of $\SubtypeSet {k}{\mathrm{and} (\operatorname{ModEq} (n , k , a), \operatorname{ModEq} (m , k , b))}$.

Nat.chineseRemainder'defMathlib.Data.Nat.ModEq, function or constant

Wording

no wording

English

Assume that $\operatorname{ModEq}$ holds for the greatest common divisor of $n$ and $m$, $a$ and $b$. Then $\operatorname{chineseRemainder'}$ applied to $h$ is an element of $\SubtypeSet {k}{\mathrm{and} (\operatorname{ModEq} (n , k , a), \operatorname{ModEq} (m , k , b))}$.

Mathlib.Data.Nat.Nth

Nat.giCountNthdefMathlib.Data.Nat.Nth, function or constant

Wording

no wording

English

Assume that $\operatorname{ofPred}$ applied to $p$ is infinite. Then $\operatorname{giCountNth}$ applied to $\mathrm{hp}$ is a Galois insertion of $\operatorname{count}$ applied to $p$ and $\operatorname{nth}$ applied to $p$ defined as the monotone intro of $\mathrm{Nat\_\_le\_nth\_count}$ applied to $\mathrm{hp}$ and $\mathrm{Nat\_\_count\_nth\_of\_infinite}$ applied to $\mathrm{hp}$.

Nat.nthdefMathlib.Data.Nat.Nth, function or constant

Wording

no wording

English

Let $p$ be a function from natural numbers to propositions. Let $n$ be a natural number. Then $\operatorname{nth}$ applied to $p$ and $n$ is a natural number defined as $\mathrm{dite}$ applied to the proposition that $\operatorname{ofPred}$ applied to $p$ is finite, the function that maps $h$ to $\operatorname{getD}$ applied to the sort of the finite set of $h$ and the function that maps $a$ and $b$ to $\mathrm{Leq} (a , b)$, $n$ and $0$ and the function that maps $h_{1}$ to $\operatorname{orderIsoOfNat}$ applied to $\operatorname{ofPred}$ applied to $p$ and $n$.

Mathlib.Data.Nat.NthRoot.Defs

Nat.nthRootdefMathlib.Data.Nat.NthRoot.Defs, function or constant

Wording

the nth root of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be natural numbers. Then the nth root of $x$ and $x_{1}$ is a natural number.

Mathlib.Data.Nat.PSub

Nat.ppreddefMathlib.Data.Nat.PSub, function or constant

Wording

no wording

English

Let $x$ be a natural number. Then $\operatorname{ppred}$ applied to $x$ is an element of $\mathrm{Option}$ applied to $\Natural$.

Nat.psubdefMathlib.Data.Nat.PSub, function or constant

Wording

no wording

English

Let $m$ and $x$ be natural numbers. Then $\operatorname{psub}$ applied to $m$ and $x$ is an element of $\mathrm{Option}$ applied to $\Natural$ defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{Nat\_\_psub\_\_\_f}$ applied to $m$.

Nat.psub'defMathlib.Data.Nat.PSub, function or constant

Wording

no wording

English

Let $m$ and $n$ be natural numbers. Then $\operatorname{psub'}$ applied to $m$ and $n$ is an element of $\mathrm{Option}$ applied to $\Natural$ defined as $\iteMACRoG {\mathrm{Leq} (n , m)}{\operatorname{some} (m - n)}{\operatorname{none}}$.

Mathlib.Data.Nat.PadicValNat

padicValNatdefMathlib.Data.Nat.PadicValNat, function or constant

Wording

the valuation of n at p (by hand)

English

Let $p$ and $n$ be natural numbers. Then $\padicValNatMACRoL {p}{n}$ is a natural number defined as the first element of the maximum power divisibility quotient of $p$ and $n$.

Mathlib.Data.Nat.Pairing

Nat.pairdefMathlib.Data.Nat.Pairing, function or constant

Wording

the pair of a and b (from the name)

English

Let $a$ and $b$ be natural numbers. Then the pair of $a$ and $b$ is a natural number defined as $\iteMACRoG {\mathrm{Lt} (a , b)}{(b \times b + a)}{(a \times a + a + b)}$.

Nat.pairEquivdefMathlib.Data.Nat.Pairing, function or constant

Wording

the pair equivalence (from the name)

English

The pair equivalence is an element of $\EquivMACRoAE {\mathrm{Prod} (\Natural , \Natural)}{\Natural}$.

Nat.unpairdefMathlib.Data.Nat.Pairing, function or constant

Wording

no wording

English

Let $n$ be a natural number. Then $\operatorname{unpair}$ applied to $n$ is an element of $\mathrm{Prod}$ applied to $\Natural$ and $\Natural$ defined as $\iteMACRoG {\mathrm{Lt} (n - \NatsqrtMACRoD {n}\times \NatsqrtMACRoD {n}, \NatsqrtMACRoD {n})}{(\ProdmkMACRoU {(n - \NatsqrtMACRoD {n}\times \NatsqrtMACRoD {n})}{\NatsqrtMACRoD {n}})}{(\ProdmkMACRoU {\NatsqrtMACRoD {n}}{(n - \NatsqrtMACRoD {n}\times \NatsqrtMACRoD {n}- \NatsqrtMACRoD {n})})}$.

Mathlib.Data.Nat.Prime.Defs

Nat.PrimedefMathlib.Data.Nat.Prime.Defs, predicate

Wording

p is prime (by hand)

English

Let $p$ be a natural number. Then $p$ is prime, if $p$ is irreducible.

Nat.PrimesdefMathlib.Data.Nat.Prime.Defs, type

Wording

prime number (by hand)

English

$\NatPrimesMACRoA$ is a set defined as $\SubtypeSet {p}{\mathrm{prime} (p)}$.

Nat.minFacdefMathlib.Data.Nat.Prime.Defs, function or constant

Wording

the smallest prime factor of n (by hand)

English

Let $n$ be a natural number. Then the smallest prime factor of $n$ is a natural number defined as $\iteMACRoG {(\divides {2}{n})}{2}{(\NatminFacAuxMACRoB {n}{3})}$.

Mathlib.Data.Nat.PrimeFin

Nat.primeFactorsdefMathlib.Data.Nat.PrimeFin, function or constant

Wording

the set of prime factors of n (by hand)

English

Let $n$ be a natural number. Then the set of prime factors of $n$ is a finite set of $\Natural$ defined as the finite set of the prime factorization of $n$.

Mathlib.Data.Nat.Squarefree

Nat.MinSqFacPropdefMathlib.Data.Nat.Squarefree, predicate

Wording

no wording

English

Let $n$ be a natural number. Let $x$ be an element of $\mathrm{Option}$ applied to $\Natural$. Then we can say that $\operatorname{MinSqFacProp}$ holds for $n$ and $x$.

Nat.minSqFacdefMathlib.Data.Nat.Squarefree, function or constant

Wording

the smallest prime factor of n (from the docstring)

English

Let $n$ be a natural number. Then the smallest prime factor of $n$ is an element of $\mathrm{Option}$ applied to $\Natural$ defined as $\iteMACRoG {(\divides {2}{n})}{(\iteMACRoG {(\divides {2}{(\frac{ n}{2})})}{\operatorname{some} (2)}{\operatorname{minSqFacAux} (\frac{ n}{2}, 3)})}{\operatorname{minSqFacAux} (n , 3)}$.

Mathlib.Data.Nat.Totient

Nat.totientdefMathlib.Data.Nat.Totient, function or constant

Wording

the totient of n (from the name)

English

Let $n$ be a natural number. Then the totient of $n$ is a natural number defined as the cardinality of $\FinsetFilter {a}{(\NatCoprimeMACRoC {n}{a})}{\FinsetrangeMACRoN {n}}$.

Mathlib.Data.Nat.Upto

Nat.UptodefMathlib.Data.Nat.Upto, type

Wording

no wording

English

Let $p$ be a function from natural numbers to propositions. Then an element of $\operatorname{Upto}$ applied to $p$ is an element of the function that maps $p$ to $\SubtypeSet {i}{\mathrm{forall} (\Natural , \lambda j . \mathrm{if} (\mathrm{Lt} (j , i), \mathrm{not} (p (j))))}$.

Nat.Upto.GTdefMathlib.Data.Nat.Upto, predicate

Wording

no wording

English

Let $p$ be a function from natural numbers to propositions. Let $x$ and $y$ be elements of $\operatorname{Upto}$ applied to $p$. Then $\operatorname{GT}$ holds for $p$, $x$ and $y$, if $x > y$.

Nat.Upto.succdefMathlib.Data.Nat.Upto, function or constant

Wording

the successor of x and h (from the name)

English

Let $x$ be an element of $\operatorname{Upto}$ applied to $p$ such that it is not the case that $p$ holds for $x$. Then the successor of $x$ and $h$ is an element of $\operatorname{Upto}$ applied to $p$ defined as the successor of $x$.

Nat.Upto.zerodefMathlib.Data.Nat.Upto, function or constant

Wording

the zero (from the name)

English

The zero is an element of $\operatorname{Upto}$ applied to $p$ defined as $0$.

Mathlib.Data.Num.Basic

NuminductiveMathlib.Data.Num.Basic, type

Wording

numerator (from the name)

English

The numerators are a basic type.

Num.adddefMathlib.Data.Num.Basic, function or constant

Wording

the sum of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be numerators. Then the sum of $x$ and $x_{1}$ is a numerator.

Num.bitdefMathlib.Data.Num.Basic, function or constant

Wording

the bit of b and x (from the name)

English

Let $b$ be an element of $\mathrm{Bool}$. Let $x$ be a numerator. Then the bit of $b$ and $x$ is a numerator defined as $\mathrm{cond}$ applied to $b$, $\operatorname{bit1}$, $\operatorname{bit0}$ and $x$.

Num.bit0defMathlib.Data.Num.Basic, function or constant

Wording

the bit of x (from the name)

English

Let $x$ be a numerator. Then the bit of $x$ is a numerator.

Num.bit1defMathlib.Data.Num.Basic, function or constant

Wording

the bit of x (from the name)

English

Let $x$ be a numerator. Then the bit of $x$ is a numerator.

Num.cmpdefMathlib.Data.Num.Basic, function or constant

Wording

the comparison of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be numerators. Then the comparison of $x$ and $x_{1}$ is an element of $\mathrm{Ordering}$.

Num.ctorElimTypedefMathlib.Data.Num.Basic, type

Wording

no wording

English

Num.divdefMathlib.Data.Num.Basic, function or constant

Wording

the quotient of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be numerators. Then the quotient of $x$ and $x_{1}$ is a numerator.

Num.div2defMathlib.Data.Num.Basic, function or constant

Wording

the quotient of x (from the name)

English

Let $x$ be a numerator. Then the quotient of $x$ is a numerator.

Num.gcddefMathlib.Data.Num.Basic, function or constant

Wording

the greatest common divisor of a and b (from the name)

English

Let $a$ and $b$ be numerators. Then the greatest common divisor of $a$ and $b$ is a numerator defined as $\iteMACRoG {\mathrm{Leq} (a , b)}{\operatorname{gcdAux} (\operatorname{natSize} (a)+ \operatorname{natSize} (b), a , b)}{\operatorname{gcdAux} (\operatorname{natSize} (b)+ \operatorname{natSize} (a), b , a)}$.

Num.moddefMathlib.Data.Num.Basic, function or constant

Wording

no wording

English

Let $x$ and $x_{1}$ be numerators. Then $\operatorname{mod}$ applied to $x$ and $x_{1}$ is a numerator.

Num.muldefMathlib.Data.Num.Basic, function or constant

Wording

the product of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be numerators. Then the product of $x$ and $x_{1}$ is a numerator.

Num.natSizedefMathlib.Data.Num.Basic, function or constant

Wording

no wording

English

Let $x$ be a numerator. Then $\operatorname{natSize}$ applied to $x$ is a natural number.

Num.ofNat'defMathlib.Data.Num.Basic, function or constant

Wording

the numerator of x (from the name)

English

Let $x$ be a natural number. Then the numerator of $x$ is a numerator defined as $\operatorname{binaryRec}$ applied to $0$, the function that maps $b$ and $x_{1}$ to $\mathrm{cond}$ applied to $b$, $\operatorname{bit1}$ and $\operatorname{bit0}$ and $x$.

Num.ofZNumdefMathlib.Data.Num.Basic, function or constant

Wording

the numerator of x (from the name)

English

Let $x$ be a numerator. Then the numerator of $x$ is a numerator.

Num.ofZNum'defMathlib.Data.Num.Basic, function or constant

Wording

the numerator of x (from the name)

English

Let $x$ be a numerator. Then the numerator of $x$ is an element of $\mathrm{Option}$ applied to the set of numerators.

Num.posconstructorMathlib.Data.Num.Basic, function or constant

Wording

the positive part of x (from the name)

English

Let $x$ be a positive part numerator. Then the positive part of $x$ is a numerator.

Num.ppreddefMathlib.Data.Num.Basic, function or constant

Wording

no wording

English

Let $x$ be a numerator. Then $\operatorname{ppred}$ applied to $x$ is an element of $\mathrm{Option}$ applied to the set of numerators.

Num.preddefMathlib.Data.Num.Basic, function or constant

Wording

the predecessor of x (from the docstring)

English

Let $x$ be a numerator. Then the predecessor of $x$ is a numerator.

Num.psubdefMathlib.Data.Num.Basic, function or constant

Wording

no wording

English

Let $a$ and $b$ be numerators. Then $\operatorname{psub}$ applied to $a$ and $b$ is an element of $\mathrm{Option}$ applied to the set of numerators defined as the numerator of the difference of $a$ and $b$.

Num.sizedefMathlib.Data.Num.Basic, function or constant

Wording

no wording

English

Let $x$ be a numerator. Then $\operatorname{size}$ applied to $x$ is a numerator.

Num.subdefMathlib.Data.Num.Basic, function or constant

Wording

the difference of a and b (from the name)

English

Let $a$ and $b$ be numerators. Then the difference of $a$ and $b$ is a numerator defined as the numerator of the difference of $a$ and $b$.

Num.sub'defMathlib.Data.Num.Basic, function or constant

Wording

the difference of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be numerators. Then the difference of $x$ and $x_{1}$ is a numerator.

Num.succdefMathlib.Data.Num.Basic, function or constant

Wording

the successor of n (from the docstring)

English

Let $n$ be a numerator. Then the successor of $n$ is a numerator defined as the positive part of the successor of $n$.

Num.succ'defMathlib.Data.Num.Basic, function or constant

Wording

the successor of x (from the docstring)

English

Let $x$ be a numerator. Then the successor of $x$ is a positive part numerator.

Num.toZNumdefMathlib.Data.Num.Basic, function or constant

Wording

the numerator of x (from the name)

English

Let $x$ be a numerator. Then the numerator of $x$ is a numerator.

Num.toZNumNegdefMathlib.Data.Num.Basic, function or constant

Wording

the numerator negation of x (from the name)

English

Let $x$ be a numerator. Then the numerator negation of $x$ is a numerator.

Num.zeroconstructorMathlib.Data.Num.Basic, function or constant

Wording

the zero (from the name)

English

The zero is a numerator.

PosNuminductiveMathlib.Data.Num.Basic, type

Wording

positive part numerator (from the name)

English

The positive part numerators are a basic type.

PosNum.adddefMathlib.Data.Num.Basic, function or constant

Wording

the sum of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be positive part numerators. Then the sum of $x$ and $x_{1}$ is a positive part numerator defined as $\operatorname{brecOn}$ applied to $x$, $\mathrm{PosNum\_\_add\_\_\_f}$ and $x_{1}$.

PosNum.bitdefMathlib.Data.Num.Basic, function or constant

Wording

the bit of b and x (from the name)

English

Let $b$ be an element of $\mathrm{Bool}$. Let $x$ be a positive part numerator. Then the bit of $b$ and $x$ is a positive part numerator defined as $\mathrm{cond}$ applied to $b$, $\operatorname{bit1}$, $\operatorname{bit0}$ and $x$.

PosNum.bit0constructorMathlib.Data.Num.Basic, function or constant

Wording

the bit of x (from the name)

English

Let $x$ be a positive part numerator. Then the bit of $x$ is a positive part numerator.

PosNum.bit1constructorMathlib.Data.Num.Basic, function or constant

Wording

the bit of x (from the name)

English

Let $x$ be a positive part numerator. Then the bit of $x$ is a positive part numerator.

PosNum.cmpdefMathlib.Data.Num.Basic, function or constant

Wording

the comparison of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be positive part numerators. Then the comparison of $x$ and $x_{1}$ is an element of $\mathrm{Ordering}$ defined as $\operatorname{brecOn}$ applied to $x$, $\mathrm{PosNum\_\_cmp\_\_\_f}$ and $x_{1}$.

PosNum.ctorElimTypedefMathlib.Data.Num.Basic, type

Wording

no wording

English

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the one and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $1$, $\mathrm{PULift}$ applied to the set of functions from positive part numerators $x$ to elements of $\mathrm{motive}$ applied to the bit of $x$ and $\mathrm{PULift}$ applied to the set of functions from positive part numerators $x_{1}$ to elements of $\mathrm{motive}$ applied to the bit of $x_{1}$.

PosNum.div'defMathlib.Data.Num.Basic, function or constant

Wording

the quotient of n and d (from the name)

English

Let $n$ and $d$ be positive part numerators. Then the quotient of $n$ and $d$ is a numerator defined as $\ProdfstMACRoZ {\operatorname{divMod} (d , n)}$.

PosNum.divModdefMathlib.Data.Num.Basic, function or constant

Wording

no wording

English

Let $d$ and $x$ be positive part numerators. Then $\operatorname{divMod}$ applied to $d$ and $x$ is an element of $\mathrm{Prod}$ applied to the set of numerators and the set of numerators defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{PosNum\_\_divMod\_\_\_f}$ applied to $d$.

PosNum.isOnedefMathlib.Data.Num.Basic, function or constant

Wording

no wording

English

Let $x$ be a positive part numerator. Then $\operatorname{isOne}$ applied to $x$ is an element of $\mathrm{Bool}$.

PosNum.mod'defMathlib.Data.Num.Basic, function or constant

Wording

no wording

English

Let $n$ and $d$ be positive part numerators. Then $\operatorname{mod'}$ applied to $n$ and $d$ is a numerator defined as $\ProdsndMACRoAA {\operatorname{divMod} (d , n)}$.

PosNum.muldefMathlib.Data.Num.Basic, function or constant

Wording

the product of a and x (from the name)

English

Let $a$ and $x$ be positive part numerators. Then the product of $a$ and $x$ is a positive part numerator defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{PosNum\_\_mul\_\_\_f}$ applied to $a$.

PosNum.natSizedefMathlib.Data.Num.Basic, function or constant

Wording

no wording

English

Let $x$ be a positive part numerator. Then $\operatorname{natSize}$ applied to $x$ is a natural number defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{PosNum\_\_natSize\_\_\_f}$.

PosNum.ofNatdefMathlib.Data.Num.Basic, function or constant

Wording

the positive part numerator of n (from the name)

English

Let $n$ be a natural number. Then the positive part numerator of $n$ is a positive part numerator defined as the positive part numerator of the predecessor of $n$.

PosNum.ofNatSuccdefMathlib.Data.Num.Basic, function or constant

Wording

the positive part numerator of x (from the name)

English

Let $x$ be a natural number. Then the positive part numerator of $x$ is a positive part numerator defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{PosNum\_\_ofNatSucc\_\_\_f}$.

PosNum.ofZNumdefMathlib.Data.Num.Basic, function or constant

Wording

the positive part numerator of x (from the name)

English

Let $x$ be a numerator. Then the positive part numerator of $x$ is a positive part numerator.

PosNum.ofZNum'defMathlib.Data.Num.Basic, function or constant

Wording

the positive part numerator of x (from the name)

English

Let $x$ be a numerator. Then the positive part numerator of $x$ is an element of $\mathrm{Option}$ applied to the set of positive part numerators.

PosNum.oneconstructorMathlib.Data.Num.Basic, function or constant

Wording

the one (from the name)

English

The one is a positive part numerator.

PosNum.preddefMathlib.Data.Num.Basic, function or constant

Wording

the predecessor of a (from the docstring)

English

Let $a$ be a positive part numerator. Then the predecessor of $a$ is a positive part numerator.

PosNum.pred'defMathlib.Data.Num.Basic, function or constant

Wording

the predecessor of x (from the docstring)

English

Let $x$ be a positive part numerator. Then the predecessor of $x$ is a numerator defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{PosNum\_\_pred'\_\_\_f}$.

PosNum.sizedefMathlib.Data.Num.Basic, function or constant

Wording

no wording

English

Let $x$ be a positive part numerator. Then $\operatorname{size}$ applied to $x$ is a positive part numerator defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{PosNum\_\_size\_\_\_f}$.

PosNum.subdefMathlib.Data.Num.Basic, function or constant

Wording

the difference of a and b (from the name)

English

Let $a$ and $b$ be positive part numerators. Then the difference of $a$ and $b$ is a positive part numerator.

PosNum.sub'defMathlib.Data.Num.Basic, function or constant

Wording

the difference of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be positive part numerators. Then the difference of $x$ and $x_{1}$ is a numerator defined as $\operatorname{brecOn}$ applied to $x$, $\mathrm{PosNum\_\_sub'\_\_\_f}$ and $x_{1}$.

PosNum.succdefMathlib.Data.Num.Basic, function or constant

Wording

the successor of x (from the docstring)

English

Let $x$ be a positive part numerator. Then the successor of $x$ is a positive part numerator defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{PosNum\_\_succ\_\_\_f}$.

ZNuminductiveMathlib.Data.Num.Basic, type

Wording

numerator (from the name)

English

The numerators are a basic type.

ZNum.absdefMathlib.Data.Num.Basic, function or constant

Wording

the absolute value of x (from the docstring)

English

Let $x$ be a numerator. Then the absolute value of $x$ is a numerator.

ZNum.adddefMathlib.Data.Num.Basic, function or constant

Wording

the sum of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be numerators. Then the sum of $x$ and $x_{1}$ is a numerator.

ZNum.bit0defMathlib.Data.Num.Basic, function or constant

Wording

the bit of x (from the name)

English

Let $x$ be a numerator. Then the bit of $x$ is a numerator.

ZNum.bit1defMathlib.Data.Num.Basic, function or constant

Wording

the bit of x (from the name)

English

Let $x$ be a numerator. Then the bit of $x$ is a numerator.

ZNum.bitm1defMathlib.Data.Num.Basic, function or constant

Wording

no wording

English

Let $x$ be a numerator. Then $\operatorname{bitm1}$ applied to $x$ is a numerator.

ZNum.cmpdefMathlib.Data.Num.Basic, function or constant

Wording

the comparison of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be numerators. Then the comparison of $x$ and $x_{1}$ is an element of $\mathrm{Ordering}$.

ZNum.ctorElimTypedefMathlib.Data.Num.Basic, type

Wording

no wording

English

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the zero and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $1$, $\mathrm{PULift}$ applied to the set of functions from positive part numerators $x$ to elements of $\mathrm{motive}$ applied to the positive part of $x$ and $\mathrm{PULift}$ applied to the set of functions from positive part numerators $x_{1}$ to elements of $\mathrm{motive}$ applied to the negation of $x_{1}$.

ZNum.divdefMathlib.Data.Num.Basic, function or constant

Wording

the quotient of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be numerators. Then the quotient of $x$ and $x_{1}$ is a numerator.

ZNum.gcddefMathlib.Data.Num.Basic, function or constant

Wording

the greatest common divisor of a and b (from the name)

English

Let $a$ and $b$ be numerators. Then the greatest common divisor of $a$ and $b$ is a numerator defined as the greatest common divisor of the absolute value of $a$ and the absolute value of $b$.

ZNum.moddefMathlib.Data.Num.Basic, function or constant

Wording

no wording

English

Let $x$ and $x_{1}$ be numerators. Then $\operatorname{mod}$ applied to $x$ and $x_{1}$ is a numerator.

ZNum.muldefMathlib.Data.Num.Basic, function or constant

Wording

the product of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be numerators. Then the product of $x$ and $x_{1}$ is a numerator.

ZNum.negconstructorMathlib.Data.Num.Basic, function or constant

Wording

the negation of x (from the name)

English

Let $x$ be a positive part numerator. Then the negation of $x$ is a numerator.

ZNum.ofInt'defMathlib.Data.Num.Basic, function or constant

Wording

the numerator of x (from the name)

English

Let $x$ be an integer. Then the numerator of $x$ is a numerator.

ZNum.posconstructorMathlib.Data.Num.Basic, function or constant

Wording

the positive part of x (from the name)

English

Let $x$ be a positive part numerator. Then the positive part of $x$ is a numerator.

ZNum.preddefMathlib.Data.Num.Basic, function or constant

Wording

the predecessor of x (from the docstring)

English

Let $x$ be a numerator. Then the predecessor of $x$ is a numerator.

ZNum.succdefMathlib.Data.Num.Basic, function or constant

Wording

the successor of x (from the docstring)

English

Let $x$ be a numerator. Then the successor of $x$ is a numerator.

ZNum.zNegdefMathlib.Data.Num.Basic, function or constant

Wording

the negation of x (from the docstring)

English

Let $x$ be a numerator. Then the negation of $x$ is a numerator.

ZNum.zeroconstructorMathlib.Data.Num.Basic, function or constant

Wording

the zero (from the name)

English

The zero is a numerator.

castNumdefMathlib.Data.Num.Basic, function or constant

Wording

the cast numerator of x4 (from the name)

English

Let $x_{4}$ be a numerator. Then the cast numerator of $x_{4}$ is an element of $x$.

castPosNumdefMathlib.Data.Num.Basic, function or constant

Wording

the cast positive part numerator of x3 (from the name)

English

Let $x_{3}$ be a positive part numerator. Then the cast positive part numerator of $x_{3}$ is an element of $x$ defined as $\operatorname{brecOn}$ applied to $x_{3}$ and $\mathrm{castPosNum\_\_\_f}$.