## Stream: new members

### Topic: Proving that C2 inside Z/n has size 2

#### Marc Masdeu (Sep 02 2020 at 15:47):

Hi,

I have defined a usually-two-element subgroup C2 of zmod n:

def C2 (m : ℕ) : subgroup (units (zmod m)) :=
{
carrier := {1, -1},
one_mem' := by simp,
mul_mem' := λ a b (ha : a ∈ {1, -1}) (hb : b ∈ {1, -1}), by finish,
inv_mem' := λ a (ha : a ∈ {1, -1}), by finish,
}


(I hope that this definition is correct. VSCode is not helping me in providing the context while writing this bit).

I want to prove that, if m > 2, then C2 (m) has size 2:

lemma one_neq_minus_one {m :  ℕ} (h : 2 < m) : \not (1 : units (zmod m)) = (-1 : units (zmod m)) :=
begin
sorry
end

lemma two_torsion_subgroup_has_two_elements {m :  ℕ} (h : 2 < m) :
fintype.card (C2 (m)) = 2 :=
begin
sorry
end


I know how to prove the first lemma, I just want to prove the second one (which has no mathematical content, given the definition of C2 and the first lemma). Any hints?

Aside: I know that @Kevin Buzzard has twitched about finset, fincard,... and what I took of it is that it was a moving target mess. Is this still the case, or there have been any changes in mathlib?

#### Reid Barton (Sep 02 2020 at 15:49):

the strategy should be something like

• fintype.card s = finset.card s
• if x \notin s then finset.card (insert x s) = finset.card s + 1
• if x \ne y then x \notin {y}

#### Reid Barton (Sep 02 2020 at 15:49):

There may also be some existing lemmas to shortcut the last steps

#### Marc Masdeu (Sep 02 2020 at 16:03):

I don't know how to write the first in Lean ( finset.card C2(p^r) does not typecheck)...

#### Marc Masdeu (Sep 02 2020 at 17:32):

Done! Thanks @Reid Barton ! It took me a while to see how these three statements would help me, but it was a neat exercise.

lemma two_torsion_subgroup_has_two_elements (h : 2 < m) :
fintype.card (C2 (m)) = 2 :=
begin
tactic.unfreeze_local_instances,
dsimp at *,
let S : finset (units (zmod m)) := {1, -1},
have H : ∀ x : units (zmod m), x ∈ S ↔ x ∈ C2 m,
{
intro x,
split;
{
intro hx,
try {rw C2_mem at hx},
finish,
}
},
suffices : finset.card S = 2,
{
rw ←this,
exact fintype.card_of_subtype S H,
},
have h1 : ∀ (x : units (zmod m)), ∀ (T : finset(units(zmod m))), (x ∉ T → finset.card (insert x T) = finset.card T + 1),
{
intros x T hx,
exact finset.card_insert_of_not_mem hx,
},
have h2 : ∀ (x y: units (zmod m)), x ≠ y → x ∉ {y} := λ {a b : units (zmod m)}, finset.not_mem_singleton.mpr,
specialize h2 1 (-1) (one_neq_minus_one h),
let S' : finset (units (zmod m)) := {-1},
specialize h1 1 S' h2,
assumption,
end


#### Yakov Pechersky (Sep 02 2020 at 18:13):

Not sure how you defined the fintype instance on C2. What's the unfreeze step for?

#### Scott Morrison (Sep 03 2020 at 03:26):

Marc Masdeu said:

(I hope that this definition is correct. VSCode is not helping me in providing the context while writing this bit).

When you're writing strutures and want more context, you can:

• use an _, and Lean will show you the expected type at that position
• use begin ... end to define a field, and you'll have the usual goal view. Usually once you've worked out what you're doing you'll want to "golf" this back to a term, if possible (at least for data fields)
• you can also build structures entirely inside tactic mode, using refine_struct { .. } or indeed just fsplit (again, you may want to golf)
• there is a hole command (type {| |}, and click on the light bulb) which can provide a "skeleton" for a structure definition, writing out the names of the fields you need to provide

#### Johan Commelin (Sep 03 2020 at 04:10):

Scott Morrison said:

Marc Masdeu said:

(I hope that this definition is correct. VSCode is not helping me in providing the context while writing this bit).

• there is a hole command (type {| |}, and click on the light bulb) which can provide a "skeleton" for a structure definition, writing out the names of the fields you need to provide

The hole command also works with _ nowadays, so you can combine this point with the first point.

Last updated: May 17 2021 at 23:14 UTC