Words, concatenation, and finiteness

Stream: new members

[Philippe Duchon]

I am very new to Lean, so I believe this should be the right place to ask novice questions.

As a personal project, I would like to prove some (supposedly easy) things on (finite) words over a (should be finite) alphabet. So, the free monoid on some type. I saw in the documentation that

List \alpha

with concatenation is the free monoid over \alpha, and this looks like a good place to start.

One lemma that I was expecting to find there is that, for any word w, the set of factorizations of w as a product of two words is a finite set - but I did not find it, very possibly because I don't know where to look. But, it might be a good exercise for me.

But, more generally, I am a bit lost with the various notions of finiteness, between Finset, Fin, Fintype, Finite... I mean, I see roughly what the different notions are, but I am not sure which is the better choice.

(Also, it looks like I don't know how to type so that \alpha becomes a nice Greek letter)

[Yaël Dillies]

Maybe look around docs#FreeMonoid