# Zulip Chat Archive

## Stream: general

### Topic: A module with a finite basis is finite

#### Riccardo Brasca (Dec 13 2021 at 13:19):

In `linear_algebra.free_module.finite.basic`

(how can I link a file and not a declaration?!) we have docs#module.finite.of_basis

```
lemma _root_.module.finite.of_basis {R : Type*} {M : Type*} {ι : Type*} [comm_ring R]
[add_comm_group M] [module R M] [fintype ι] (b : basis ι R M) : module.finite R M :=
```

I wrote this, but I don't remember why I made it a lemma and not an instance. The easiest reason is that if it is an instance we get an error in docs#module.End.supr_generalized_eigenspace_eq_top

```
eigenspace.lean:526:4
maximum class-instance resolution depth has been reached
```

I don't see the problem, I tried with `set_option trace.class_instances true`

, but the output is too long. Does someone see what is going wrong?

#### Johan Commelin (Dec 13 2021 at 13:20):

`module.finite R M`

doesn't mention the basis `b`

.

#### Johan Commelin (Dec 13 2021 at 13:20):

So the TC system has no way to find it.

#### Johan Commelin (Dec 13 2021 at 13:22):

*If* there was also some form of forward search, which sees `basis ι R M`

in your context, and finds `[fintype ι]`

and consequently invokes this instance, then that would be great. But that's not how TC inference works in Lean 3. It only works backwards from the goal.

#### Riccardo Brasca (Dec 13 2021 at 13:24):

Ah, I see, I thought it was somehow creating a loop.

#### Riccardo Brasca (Dec 13 2021 at 13:41):

In #10757 I've added the instance at least for `fin n → R`

, that seems very reasonable. (Indeed it golfs at least one proof.)

#### Johan Commelin (Dec 13 2021 at 13:42):

Yeah, you can certainly add instances for special cases.

#### Johan Commelin (Dec 13 2021 at 13:43):

You can even generalize `fin n`

to `ι`

+ `[fintype ι]`

.

#### Yury G. Kudryashov (Dec 13 2021 at 13:51):

Do we have an instance for `Π i, M i`

with `[fintype ι]`

`[∀ i, module.finite R (M i)]`

?

#### Yury G. Kudryashov (Dec 13 2021 at 13:52):

We already have https://leanprover-community.github.io/mathlib_docs/linear_algebra/finite_dimensional.html#finite_dimensional.finite_dimensional_pi

#### Riccardo Brasca (Dec 13 2021 at 14:00):

`finite_dimensional`

is now defined to be `module.finite`

, so in #10757 I generalize docs#finite_dimensional.finite_dimensional_pi (that is for `division_ring`

to any `comm_ring`

. It is a `Prop`

, so I don't think it is a problem to have both of them.

Sooner or later I will refactor `linear_algebra.finite_dimensional`

to move all the generalizable results to `linear_algebra.free_module.finite.*`

but it is quite a bit of work because of some problems with the import structure.

#### Riccardo Brasca (Dec 13 2021 at 14:00):

I wanted to do it one or two months ago but then I got absorbed by `flt-regular`

...

#### Riccardo Brasca (Dec 13 2021 at 14:02):

OMG I forgot to update the docstring of docs#finite_dimensional, that still says "finite_dimensional vector spaces are defined to be noetherian modules"?! :scream:

#### Riccardo Brasca (Dec 13 2021 at 14:02):

Let me fix it.

#### Riccardo Brasca (Dec 13 2021 at 14:09):

#10758 (this PR is just a couple of lines)

#### Floris van Doorn (Dec 14 2021 at 16:36):

Riccardo Brasca said:

`linear_algebra.free_module.finite.basic`

(how can I link a file and not a declaration?!)

file#linear_algebra/free_module/finite/basic

#### Riccardo Brasca (Dec 14 2021 at 16:53):

Thanks!

Last updated: Dec 20 2023 at 11:08 UTC