Pedagogical arguments for/against the "defineorem" (simultaneously definition and theorem)

Question

Often times, we like to define things in ways that are not obviously possible. For example, we may define something to be the unique object satisfying a certain property, or we may want to state many equivalent definitions of the same object. Such definitions require a theorem proving the correctness. When lecturing or writing notes/books, there seem to be two common ways of dealing with this issue:

1. First prove the theorem without defining the term, then define the term as "the object from the previous theorem." This has many issues: the motivation for the theorem may seem weak, and the location of the real definition is physically far from the heading "Definition (object)." (i.e. there is a big proof in between).
2. First define the term in an unambiguous way, then state and prove the theorem that it is equivalent to other characterizations. This also has issues: it may (wrongly) suggest that the initial definition is more important or standard than others, whereas it may actually be the least useful for the sake of being unambiguous.

Of course, the motivation issues can be resolved by surrounding the mathematical content with sufficient prose, but this needlessly makes the lecture or text take longer because many things must be repeated. However, one can imagine avoiding all of these problems by just using the term "defineorem" and writing something like the following:

Defineorem 1.2 (determinant). The determinant on $n$ dimensions is the unique multilinear, skew-symmetric function $\det_n : \operatorname{Mat}_{n \times n}(\mathbb{F}) \to \mathbb{F}$ satisfying $\det_n(I_n) = 1$. We write $\det$ for $\det_n$ when there is no confusion.

If the proof is long, it feels normal here to ask students/readers to accept the result for a minute and see a few quick examples/applications first, as is common for other big theorems. Then the proof is written:

Proof of Defineorem 1.2. Here is the proof.

My question is this: Are there any pedagogical or technical reasons for why/when defineorems should be avoided? Conversely, it would also be interesting to hear other arguments for expanding the use of defineorems.

Answer 1

The problem with all three approaches you sketch is that they force you to put the theorem quite early in the development, even though it may be pretty heavy going to start with it without any chance to develop any intuition yet. Your "defineorem" gives you a bit of breathing space, but it still sounds like you'd prefer not to have any other numbered definitions/theorem come between the initial statement and its proof.

For pedagogy, how about this:

Definition 1.2 (determinant). A determinant is a function $\mathrm{Mat}_{n\times n}(\mathbb F)\to \mathbb F$ which is multilinear in rows and columns, skew-symmetric, and maps $I_{n\times n}$ to $1_{\mathbb F}$.

We shall see later (Theorems 1.23 and 1.24) that there exists exactly one determinant function for each $n$ and $\mathbb F$, at which point "a determinant" will become "the determinant". For now let's explore a few simple examples of determinants: $$ \mathrm{det}_1 : \mathrm{Mat}_{1\times 1}(\mathbb R) \to \mathbb R: \begin{bmatrix} a \end{bmatrix} \mapsto a \\ \mathrm{det}_2 : \mathrm{Math}_{2\times 2}(\mathbb R) \to \mathbb R: \begin{bmatrix} a & b \\ c & d \end{bmatrix} \mapsto ad-bc $$

... bla bla bla ...

Theorem 1.23. The following recursive definition defines a determinant for every dimension: $$\textit{(e.g., expansion by minors)}$$

Theorem 1.24. Every determinant is identical to one of the functions defined in Theorem 1.23. In particular the determinant for every dimension is unique.

This will give the reader some concrete examples to keep in mind while you develop consequences of the definition, and you'll have mostly free rein to prove the general existence and uniqueness at the appropriate point in the development.