finite_free

Stream: condensed mathematics

[Scott Morrison]

I notice a TODO in finite_free.lean (that @Kevin Buzzard has been working on), about making another version of finite_free for modules. Is the version for groups actually needed, or could we get by with just the one for modules, specializing to int when needed?

[Scott Morrison]

I killed the sorries in rank_zero and rank_dual.

[Johan Commelin]

@Scott Morrison Now that the int_smul refactor is done, I think there is a lot less need to do finite_free for groups. But I guess occasionaly we would need it for multiplicative groups? (Dirichlet unit theorem in number theory...)

[Johan Commelin]

Anyway, I think it ought to be split up: module.finite (which we already have) and module.free.

[Scott Morrison]

It makes me so sad we still don't have Smith normal form in mathlib... It's been doable for years!

[Scott Morrison]

Unfortunately the induction has many layers.

[Kevin Buzzard]

We don't need SNF to prove the structure theorem for fg modules over a PID, right? This is more like some algorithm to work out the actual generators?

[Scott Morrison]

No, it's not necessary, although it does provide a nice proof.