[Merged by Bors] - feat: Cardinal of GLn with coefficients in a finite field

[ThomasLanard]

---

We add the cardinal of the general linear group GLn with coefficients in a finite field.

[github-actions]

PR summary 5ad36cbcc7

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card	1207

---

Declarations diff

+ card_GL_field
+ card_linearIndependent
+ equiv_GL_linearindependent
+ equiv_linearIndependent

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[CBirkbeck]

I've left some comments on the code, it looks pretty good to me, only some minor fixes/golfing.

[ThomasLanard]

Thank you! I've made the corrections that were suggested.

[grunweg]

Coming here for issue triage: it seems you're looking for review on this PR; I have labelled it awaiting-review accordingly.
Also note that this PR cannot be merged while it is in draft mode. If you consider it ready for review, would you like to un-draft it? (Draft PRs also do not show up in the review queue.)

[riccardobrasca]

Can you please mark "resolved" the comments that you took into account?

There is also an error related to imports (this should be very easy to resolve). Thanks!

[riccardobrasca]

Thinking a little bit more about it, maybe you can use Nat.card and completely avoid various Fintype instances. It seems to me the best way of doing stuff. Note that you may need the instances in proofs (to make the link between Nat.card and Fintype.card, that has a better API), but there is no need to create global instances.

[ThomasLanard]

Thinking a little bit more about it, maybe you can use Nat.card and completely avoid various Fintype instances. It seems to me the best way of doing stuff. Note that you may need the instances in proofs (to make the link between Nat.card and Fintype.card, that has a better API), but there is no need to create global instances.

I changed the Fintype.card into Nat.card and suppressed all the instances (hence, also the modification in the file about Clifford algebra).

[riccardobrasca]

I've investigated what's happening here, and the problem is that you are changing the structure of the import graph, and this is making things too slow in other files that import GeneralLinearGroup. My suggestion is to create a new folder GeneralLinearGroup, with files Basic (corresponding to what already is in master) and a file Card, where you can put your result, importing whatever you need. We have a command find_home to see where we can put files without changing the imports and it seems impossible to do so for your card_LinearInependent_subtype.

[riccardobrasca]

Even better, we may have three files: Defs, Basic and Card, this is what we usually do nowadays. Maybe a preliminary PR doing the split is the way to go.

[ThomasLanard]

After thinking about it, I found it a bit weird to split the GeneralLinearGroup.lean file into a folder. For instance, there is also a SpecialLinearGroup.lean file and not a folder. Thus instead I added a Card.lean file into the folder Matrix which could contain different statements about cardinals of subsets of matrices. For instance, I added a simple result about the cardinal of the set of matrices over a finite field.

I moved equiv_linearIndependent to Mathlib.LinearAlgebra.LinearIndependent. But I don’t know where to put card_linearInependent.

[riccardobrasca]

What I am proposing is to split the existing file GeneraliLinearGroup into two files GeneraliLinearGroup.Defs and ``GeneraliLinearGroup.Basic, and then add a file GeneraliLinearGroup.Card` containing your result. It's better to do the splitting in another PR (this kind of PRs are usually reviewed very quickly since nothing has really changed), and then updating this one. I know it looks a slow process, but mathlib is a huge library, and it is better to waste some time but doing things properly.

I can do it you want.

[riccardobrasca]

Now the file should go in the GeneralLinearGroup folder.

[riccardobrasca]

Thanks!

bors d+

[mathlib-bors]

✌️ ThomasLanard can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[CBirkbeck]

Thanks for doing all of this!

[riccardobrasca]

Interesting that we don't need commutativity for the formula to hold (I know commutativity is secretly there, but we don't need to know it).

[ThomasLanard]

Interesting that we don't need commutativity for the formula to hold (I know commutativity is secretly there, but we don't need to know it).

I have imported Mathlib.RingTheory.LittleWedderburn to have commutativity! It is the only reason for this import.

[riccardobrasca]

Interesting that we don't need commutativity for the formula to hold (I know commutativity is secretly there, but we don't need to know it).

I have imported Mathlib.RingTheory.LittleWedderburn to have commutativity! It is the only reason for this import.

Oh, I didn't notice it. I suggest to not import it and prove it for Field then.

[ThomasLanard]

Thank you!

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style