Definitions which should be propositions/theorems I am asking for a list of concepts which some sources present as definitions whereas other sources pose them as propositions/theorems.
For example, most abstract algebra books will define a group isomorphism to be a bijective group homomorphism. However, after one is introduced to category theory, one realizes that it is an ever-so-slightly non-trivial result that isomorphisms in Grp are precisely the bijective group homomorphisms.
Another example is a $C^k$ differentiable manifold. It is a theorem that every maximal atlas of a $C^k$ differentiable manifold ($k>0$) contains a $C^\infty$ atlas. And thus, the nuances in the terms '$C^k$ differentiable manifold' and 'smooth manifold' are not discussed in some sources.
The final example I'll point out is analytic vs. holomorphic complex functions. I've seen books define holomorphic functions and then say 'analytic' is just a synonym. Whereas I believe that it should be a theorem that every holomorphic function is analytic (where analytic is of course defined to be 'representable by a convergent power series').
The problem with these examples is that without the proper background, I could live my life blissfully ignorant with using these terms as definitions. But I believe that this also robs me of seeing a beautiful result which hints at deep subtleties. So I am asking the community to share their knowledge of other such examples they may have encountered.
 A: A finite extension of fields $k\subset K$ is Galois if it diagonalizes itself: the $K$-algebra $K\otimes_k K$ is isomorphic to the split $K$-algebra $K\times...\times K$.
A finite covering of topological spaces $X\to Y$ is normal if it trivializes itself: the covering $X\times _Y X\to X$ is homeomorphic  to the trivial covering $X\sqcup...\sqcup X\to X $.  
These awesomely similar non-standard  definitions are due to Grothendieck who introduced a fantastic theory of  coverings generalizing (in spirit at least) both.
For details, see this most original book (not translated, alas).
A: There are lots of examples. But since I'm in hurry, here is just one:
A homomorphism of groups should be defined as a map which is compatible with the whole group structure, i.e. multiplication, inverse and neutral element. It is then a Lemma then it suffices to prove this for multiplication. Notice that we don't have such a Lemma for monoid (or ring) homomorphisms, we don't get the neutral element for free.
A: I think that most introductions to the determinant are written in a very misleading way—they define the determinant using a formula or an algorithm, then gradually prove that it has various nice properties.  This makes it seem as though facts like $\operatorname{det}AB=(\operatorname{det}A)(\operatorname{det}B)$, $\operatorname{det}A=\operatorname{det}A^T$, or "$\operatorname{det}$ is linear in each row" are nontrivial, and makes the definition itself seem unmotivated.
Really, the one major nontrivial theorem about determinants is that they exist—that is, some function exists on the set of $n\times n$ matrices which is linear in each row, vanishes when two rows are equal, returns $1$ for the identity matrix, etc.  The various "definitions" of the determinants are easy to understand as consequences of these properties, but, pedagogically, they should appear after those properties are introduced, not before.
To further illustrate this example, consider the determinant when restricted to permutation matrices, which is just the sign function on permutations, $\epsilon: S_n \to \{\pm 1\}$ (and since I like stirring up controversy, I'll also mention that $\epsilon$ is the determinant on the set of $n\times n$ matrices over the field $\mathbb{F}_1$).
It is not obvious from the definitions that the sign of a permutation exists, i.e. that each $S_n$ ($n\geq 2$) has a normal subgroup of index $2$.  I'm not saying it's a difficult theorem, but there's definitely something that needs proving, namely: if a product of $k$ transpositions equals a product of $l$ transpositions, then $k$ and $l$ have the same parity.  Technically we can define $\epsilon(\sigma)$ to be $(-1)^{q_\sigma}$, where $q_\sigma$ is the number of pairs from $\{1,2,\ldots,n\}$ which are out of order, then use its properties to prove that $\epsilon$ is a homomorphism... but in my opinion, this definition is only motivated within the attempt to prove that there exists a homomorphism $\epsilon$ with certain properties.
(By contrast, something like the existence of "the" tensor product or "the" algebraic closure is usually handled correctly, in my experience—we give definitions to say what properties we want these things to have, then only give concrete forms for them when we need to prove that they exist.)
