## Stream: new members

### Topic: intro Jan de Wit

#### Jan de Wit (Mar 13 2021 at 21:02):

Hello everybody!

I'm Jan de Wit, from Utrecht in the Netherlands. I have a fairly strong mathematical but mostly CS (Haskell) background (@Andres Löh might remember me from way back when in the Generic Haskell days...). Nowadays I work in IT, but that's not going to stop me from tickling my brain from time to time; and Lean seems just the ticket.

So to kick things off, I've got two questions; one CS-y and one mathematical.

1: Is there a formal definition of the Lean language, something like to the Haskell reports? The sheer amount of syntax overwhelms me at times, but that's probably due to me not knowing the "prelude" by heart....

2: How would I go about proving that a group with 4 elements is either isomorphic to Z_4 or Z_2 x Z_2? I've followed the 'Formalising Mathematics' series of blog posts by @Kevin Buzzard up to week 6, but I don't even know how to state the hypothesis that the carrier is finite and has 4 elements. I also don't know how to construct cyclic groups or direct products. And finally I don't want to do a case analysis on the 4^16 possible multiplication tables :-) I don't need (or want!) a slick proof, I just want to know where to start. ..

#### Johan Commelin (Mar 13 2021 at 21:04):

Welcome! Always good to have more Dutchies on board :grinning:

#### Johan Commelin (Mar 13 2021 at 21:05):

example (G : Type*) [fintype G] (h : fintype.card G = 4) : ...


#### Johan Commelin (Mar 13 2021 at 21:05):

There you have a type with 4 elements

#### Johan Commelin (Mar 13 2021 at 21:09):

docs#prod.group gives you product groups and docs#is_cyclic cyclic groups

#### Eric Wieser (Mar 13 2021 at 21:21):

I think this might be one way to state your theorem for 2:

import data.zmod.basic
import data.fintype.basic

example (G : Type*) [fintype G] [add_group G] (h : fintype.card G = 4) :
nonempty (G ≃+ zmod 4) ∨ nonempty (G ≃+ zmod 2 × zmod 2) := sorry


where docs#add_equiv ≃+ is your "isomorphic", and docs#zmod is your Z_n

#### Thomas Browning (Mar 13 2021 at 21:22):

And if you want to classify groups of order 4 (or p^2) for that matter, you might find docs#order_of helpful

#### Jan de Wit (Mar 13 2021 at 21:23):

Hi Johan, thanks for the welcome! I'll go and poke around in mathlib some more tomorrow, you've given me the first steps :-) I guess I'm still stumbling around due to a lack of discoverability - I know it's probably there, but I just don't know where to look.

#### Thomas Browning (Mar 13 2021 at 21:24):

Is there a cyclic multiplicative group in mathlib? As soon as you go to groups of order 6, you're going to want to work with multiplicative groups rather than additive groups.

#### Eric Wieser (Mar 13 2021 at 21:24):

multiplicative (zmod n) is the multiplicative version

#### Eric Wieser (Mar 13 2021 at 21:25):

But does it matter? All it changes is whether you use the symbols +/- or *//.

#### Thomas Browning (Mar 13 2021 at 21:26):

if you're working with nonabelian groups, then * seems like a better option. For example, the symmetric groups are multplicative, I think.

#### Thomas Browning (Mar 13 2021 at 21:26):

(e.g. equiv.perm (fin n))

#### Thomas Browning (Mar 13 2021 at 21:27):

Technically there's no difference, but morally I feel like you should be using *

#### Jan de Wit (Mar 13 2021 at 21:30):

Eric Wieser said:

nonempty (G ≃+ zmod 2) ∨ nonempty (G ≃+ zmod 2 × zmod 2) := sorry



(Your first 2 should be a 4, right?)
Ahh, I get it, I think.  G  ≃+ H is the *type* of additive isos between G and H, not the proposition that there exists such an iso.


#### Alex J. Best (Mar 13 2021 at 21:31):

Jan de Wit said:

Hi Johan, thanks for the welcome! I'll go and poke around in mathlib some more tomorrow, you've given me the first steps :-) I guess I'm still stumbling around due to a lack of discoverability - I know it's probably there, but I just don't know where to look.

https://leanprover-community.github.io/learn.html is the place to start if you haven't seen it, but there is a lot on there! The tactic cheat sheet https://leanprover-community.github.io//img/lean-tactics.pdf might be the sort of thing you are looking for, with some of the most common tactics.
For example I imagine your proof will start with something like by_cases h : \exists g : G, g.order_of = 4,.
The issue with having a completely definitive reference is that tactics can take almost arbitrary syntax, so to know the language completely you'd have to read all of https://leanprover-community.github.io/mathlib_docs/tactics.html which is way too long!

#### Jan de Wit (Mar 13 2021 at 21:36):

@Alex J. Best : I studied under Swierstra so I know monadic parsers when I see 'em :-) The flexibility of Lean's syntax makes me go down rabbit holes which leave me wanting for clearer docstrings :-)

#### Johan Commelin (Mar 13 2021 at 21:36):

@Jan de Wit I think the search bar on the docs page is quite useful, and good ol' grep (-;

#### Thomas Browning (Mar 13 2021 at 21:43):

And the plain search feature in VS Code

#### Jan de Wit (Mar 13 2021 at 21:59):

@Johan Commelin and all the rest: Thank you all for the help, I know what I'll be doing tomorrow!

PS: can you parametrize over x/+/foo? It seems a waste of namespace to have to use ≃, ≃+ and ≃foo etcetera, when the operation is a parameter. I know there's a (rather brute-force) tactic that lifts multiplicative proofs to additive ones for groups somewhere, but it seems to me that once you want to express statements like the (x,inv,1/+,neg,0/foo,bar,baz) group on the left is isomorphic to the (x/+/foo) group on the right you get a quadratic explosion of statements, all rather devoid of content :-)

#### Scott Morrison (Mar 13 2021 at 22:31):

Jan de Wit said:

... go down rabbit holes which leave me wanting for clearer docstrings :-)

This is perhaps an unhelpful thing to say to a newcomer, but we love PRs adding docstrings, and, sometimes the person most able to add good ones is the person who has just now deciphered what the function is doing. (But also, our collective apologies: we know docstrings need to be better.)

#### Scott Morrison (Mar 13 2021 at 22:42):

Jan de Wit said:

Johan Commelin and all the rest: Thank you all for the help, I know what I'll be doing tomorrow!

PS: can you parametrize over x/+/foo?

• as it turns out, there's less foo than you might expect, and mathematicians have pretty robust opinions about what is + and what is * (but of course we have order equivalences, and perhaps soon lattice equivalences, etc etc)
• yes, the category theory library has a polymorphic notion of equality, and you can write G ≅ H (with the same iso behind that notation), whether G H : AddCommGroup or G H : cochain_complex (Mon_ (sheaf X Ring)). But:
• this is not actually as polymorphic as the existing ≃+, because it requires G and H to be in the same universe. (My universe is Type 0...)