5. Bodyless TeX statement
Some imports start from TeX rather than Markdown. This node has no native Verso body and no Markdown witness, but it still gets a TeX badge, source provenance, and a Lean declaration preview.
Definition5.1
Rendered from external TeX source (statement): source/imported-paper.tex:88:0-96:0; no native Verso body is available.
\begin{definition}\label{def:imported-multiplication}
The imported TeX source defines the multiplication operation used by the later
results in this section.
\end{definition}
Lean code for Definition5.1●1 definition
Associated Lean declarations
-
Nat.mul[complete]
Associated Lean declarations
-
Nat.mul[complete]
-
defdefined in Init/Prelude.leancomplete
def Nat.mul : Nat → Nat → Nat
def Nat.mul : Nat → Nat → Nat
Multiplication of natural numbers, usually accessed via the `*` operator. This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.