Zulip Chat Archive

Stream: maths

Topic: group theory: lagrange theorem


view this post on Zulip 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!

view this post on Zulip 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"!

view this post on Zulip Heather Macbeth (Mar 06 2021 at 03:00):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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