## Stream: general

### Topic: definition depending on theorem

#### Johan Commelin (Oct 08 2018 at 06:30):

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 (Oct 08 2018 at 06:34):

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

#### Mario Carneiro (Oct 08 2018 at 06:43):

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 (Oct 08 2018 at 07:04):

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 (Oct 08 2018 at 07:06):

at the expense of computability of course

#### Kevin Buzzard (Oct 08 2018 at 08:10):

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 (Oct 08 2018 at 08:10):

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