# Zulip Chat Archive

## Stream: maths

### Topic: group theory: lagrange theorem

#### François Sunatori (Mar 06 2021 at 02:18):

Hi,

I'm somewhat new to Lean and am trying to find a place to contribute in Lean and realized that group-theory-game (https://github.com/ImperialCollegeLondon/group-theory-game) has a proof for the Lagrange theorem but I couldn't find it in Mathlib. Is there a reason why it isn't currently in Mathlib or if it is could someone tell me where I can find it? If it isn't yet in Mathlib I'm hoping that maybe it could be a good project for me to start with. Any thoughts?

Thank you!

#### Bryan Gin-ge Chen (Mar 06 2021 at 02:42):

docs#card_subgroup_dvd_card is one possible statement of Lagrange's theorem. It could definitely use a docstring mentioning "Lagrange"!

#### Heather Macbeth (Mar 06 2021 at 03:00):

@François Sunatori What is your background? What areas do you know well?

#### François Sunatori (Mar 06 2021 at 03:13):

Hi @Heather Macbeth, I have a bachelors degree in Computer Science and Mathematics and I have a particular interest in abstract algebra and algebraic number theory. I also enjoyed graph theory during my studies.

#### Heather Macbeth (Mar 06 2021 at 03:32):

@François Sunatori Welcome! We have a page

https://leanprover-community.github.io/undergrad_todo.html

of undergrad-level topics missing from mathlib. Although before starting to work on one of them you should beware that some of them are "missing from mathlib" for stupid reasons, for example there is a high-powered version in mathlib that hasn't yet been translated to elementary form.

Here's a little lemma that's not on that list but which I noticed the other day was missing: an isometry of `ℂ`

fixing 0 is a rotation or reflection.

```
import analysis.complex.basic
open complex
local notation `|` x `|` := complex.abs x
lemma linear_isometry_complex (f : ℂ →ₗᵢ[ℝ] ℂ) :
∃ a : ℂ, |a| = 1 ∧ ((∀ z, f z = a * z) ∨ (∀ z, f z = a * conj z)) :=
begin
sorry
end
```

#### Heather Macbeth (Mar 06 2021 at 03:36):

And its corollary: a finite subgroup of the group of isometries of `ℂ`

fixing 0 (use docs#linear_isometry_equiv.group) is isomorphic to either docs#zmod or docs#dihedral.

#### François Sunatori (Mar 06 2021 at 03:50):

Oh I didn't know about https://leanprover-community.github.io/undergrad_todo.html!

I think `linear_isometry_complex`

is a good place for me start. Thanks for the suggestions :) @Heather Macbeth !

Last updated: May 12 2021 at 08:14 UTC