Number of k-dim subspaces

Stream: Is there code for X?

[Alena Gusakov]

Hi, is there anything in mathlib that counts the number of k-dimensional subspaces of a vector space over a finite field? I didn't see anything like it but in the past week I've accidentally wasted time reproving things that already existed twice, and I want to make sure it hasn't been proven yet before I get burned again. Thanks!

[Jireh Loreaux]

To be clear you want to compute something like this (the cardinality of the Grassmannian)?

lemma card_submodule_of_dim (F V : Type*) [field F] [fintype F] [add_comm_group V] [module F V]
  [finite_dimensional F V] (k : ℕ) :
  nat.card { S : submodule F V // finite_dimensional.fin_rank K S = k } = something :=
sorry

[Jireh Loreaux]

If so, I can't find anything like that.

[Alena Gusakov]

Yeah, exactly that!

[Eric Wieser]

Presumably given a basis for V you could explicitly enumerate them?

[Alena Gusakov]

I was thinking of doing that, but my current approach was more along the lines of showing that the nonzero elements of V are partitioned by the 1-dimensional subspaces (I'm proving it for 1-dim subspaces first to make it easier) and then counting the cardinalities

[Alena Gusakov]

But yeah the proof for general dimension k is usually counting linear combinations, i.e. enumerating using a basis

[Alena Gusakov]

The problem is when you have scalar multiples of a vector they all map to the same subspace, so you have to divide to account for that

[Richard Copley]

These are the q-deformed binomial coefficients, https://math.ucr.edu/home/baez/week184.html (and week 188). Not sure that helps you but it's fun.

[Martin Dvořák]

(deleted)