# Zulip Chat Archive

## Stream: maths

### Topic: finite_dimensional assumption

#### Patrick Lutz (Sep 21 2020 at 23:52):

Why does `findim_top`

(documentation) require that the vector space is `finite_dimensional`

? If I'm understanding things correctly, it should be true in general. Is it because it's only coincidentally true if the vector space is finite dimensional (because it depends on the arbitrary decision of how to define `findim`

for infinite dimensional vector spaces) and therefore it's bad to prove it? For reference, `findim_top`

says

```
theorem findim_top [finite_dimensional K V] : findim K (⊤ : submodule K V) = findim K V
```

In general, when mathlib includes arbitrary definitions meant to make a function total (like dividing by zero, or findim of infinite dimensional vector spaces), when is it reasonable to prove theorems that only work because of some particular details of that arbitrary definition?

#### Patrick Lutz (Sep 21 2020 at 23:53):

Also sorry if "maths" is not the right stream for this question. I wasn't really sure which stream it belonged in. Maybe "new members" but I feel like at some point I should stop posting questions there.

#### Mario Carneiro (Sep 21 2020 at 23:53):

I assume the author didn't bother to consider the infinite dimensional case

#### Patrick Lutz (Sep 21 2020 at 23:53):

Is it reasonable for me to add it?

#### Mario Carneiro (Sep 21 2020 at 23:54):

sure

#### Patrick Lutz (Sep 21 2020 at 23:54):

I want to add some lemmas about dimensions of `subalgebra`

s and this will make it slightly easier

#### Mario Carneiro (Sep 21 2020 at 23:55):

I assume `findim`

is some operator applied to `dim`

? If so the proof should be easy if you have `dim K top = dim K V`

#### Patrick Lutz (Sep 21 2020 at 23:57):

Yeah, that's true

Last updated: May 09 2021 at 11:09 UTC