group theory: lagrange theorem

Stream: maths

[François Sunatori]

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]

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

[Heather Macbeth]

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

[François Sunatori]

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]

@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]

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]

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 !