finite_dimensional assumption

Stream: maths

[Patrick Lutz]

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]

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]

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

[Patrick Lutz]

Is it reasonable for me to add it?

[Mario Carneiro]

sure

[Patrick Lutz]

I want to add some lemmas about dimensions of subalgebras and this will make it slightly easier

[Mario Carneiro]

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]

Yeah, that's true