definition depending on theorem

Stream: general

[Johan Commelin]

For my Lean-talk I would like a good example of a definition that depends on a (non-trivial) theorem. I don't want to use perfectoid spaces because that is way too advanced. I want to use this thread to collect a list of cute examples.

[Bryan Gin-ge Chen]

How about: the dimension of a vector space depending on the fact that all bases have the same cardinality

[Mario Carneiro]

technically, the definition doesn't need this assumption, because it is defined as the minimum of such cardinalities. Instead, a proof is required to show that a minimum of cardinalities is well defined

[Chris Hughes]

convergence of exponential series. Also proof that the polynomial division algorithm is well founded took me a while. All of these can be done without any proofs technically, with some dite statement.

[Mario Carneiro]

at the expense of computability of course

[Kevin Buzzard]

The definition of an affine scheme needs the fact that the structure sheaf on $Spec(A)$ is actually a sheaf, which took us quite some time to prove.

[Johan Commelin]

Yes, but I will be talking to an audience that partly doesn't know what a sheaf is...

[Patrick Massot]

What about the definition of addition of real numbers? Or even addition or integers