## 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?

sure

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

I want to add some lemmas about dimensions of subalgebras 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