Submitting code related to dihedral groups

Stream: new members

[Alex Griffin]

As some of you could probably guess from my repeated questions about dihedral groups, I've been working with them in Lean. I have a few results that I think would be good additions to mathlib's dihedral group file. Specifically, I have work related to which elements can and cannot be central in a (non-degenerate) dihedral group, since this is a result not already contained in mathlib's dihedral group file that would be commonly desired among people working with them. Now, before I officially ask for permission to make a pull request, I have uploaded the code I wrote in a standalone Lean file to my GitHub page (I am Fontkodo on GitHub), so that it could be reviewed, in case there is something wrong with it. The file can be found here. Note that while the code is contained in a standalone file, this is just for presentation purposes, because the intent is that these result would be added to the existing file. Please let me know if there is something that should be improved upon before I submit a pull request.

[Bryan Gin-ge Chen]

I've sent you an invite: https://github.com/leanprover-community/mathlib/invitations

Your code looks ready enough to PR (though I can't guarantee that what you've proved isn't hidden somewhere else). It's generally easiest for us to review contributions in the form of a PR since we can easily add comments and suggestions and also have our scripts check whether the code builds, etc.

[Damiano Testa]

Hi Alex,

I have not looked at the groups part of mathlib. However, if you are interested, below is a golfed version of your lemmas.

I changed the existential lemmas with the explicit element used, since it seemed stronger to actually have a witness, rather than a mere existential statement.

lemma sr_not_mem_center [fact (n > 2)] (i : zmod n): sr i * (r 1) ≠ (r 1) * r i :=
by simp

/--
Rotations with order greater than 2 are not central.
`i` is any `zmod n` term satisfying `2 * i ≠ 0`.
-/
theorem r_not_mem_center {i : zmod n} (h : 2 * i ≠ 0) : r i * (sr 1) ≠ (sr 1) * r i :=
by simpa [sub_eq_add_neg, ← add_eq_zero_iff_neg_eq, ← two_mul]

/--
Rotations with order at most 2 commute with all rotations.
`i` is any `zmod n` term satisfying `2 * i = 0`.
-/
theorem r_mem_center_r {i : zmod n} (h : 2 * i = 0) (j : zmod n) : r i * r j = r j * r i :=
by simp [add_comm]

/--
Rotations with order at most 2 commute with all reflections.
`i` is any `zmod n` term satisfying `2 * i = 0`.
-/
theorem r_mem_center_sr {i : zmod n} (h : 2 * i = 0) (j : zmod n) : r i * sr j = sr j * r i :=
by simpa [sub_eq_add_neg, ← add_eq_zero_iff_neg_eq, ← two_mul]