## Stream: new members

### Topic: Dealing with finite set of units of a ring

#### Jamie Reason (Jul 26 2022 at 10:50):

Hi there! I'm learning Lean and trying to prove an example that there are no comm rings with 5 units. I've shown that the group of units is cyclic, but trying to introduce it's generator element u,

1. Is there a way I can use this to refer to all the units as powers of u? where 1 = u^5
2. How can I also use u for ring operation "+" when u has type Rˣ and not R

I looked at subgroup.zpowers in group_theory.subgroup.basic but can't figure out how Lean is treating these objects.
My code is below but note I don't want spoilers for the later part of this problem.

import algebra.ring.basic
import ring_theory.int.basic
import group_theory.specific_groups.cyclic
import data.fintype.basic

theorem no_5_unit_comm_ring {R : Type*} [comm_ring R] [fintype Rˣ] : fintype.card (Rˣ) ≠ 5 :=
begin
intro h5u, -- assume we have a ring with 5 units for a contra

-- group of units Rˣ is cyclic
have h : is_cyclic Rˣ, {
apply is_cyclic_of_prime_card _,
{ use _inst_2 },
{ use 5 },
{ norm_num,
exact {out := trivial } },
{ exact h5u },
},

--can view Rˣ as {1, u, u², u³, u⁴} (multiplicative group)
cases h,
cases h with u hu,

have h1 : 1 = u^5, {
sorry
},

--(1 + u + u²)(u + u² + u⁴) = (u + u⁶) + (u² + u²) + (u⁴ + u⁴) + (u³ + u³) + u⁵ = 2(u + u² + u³ + u⁴) + 1
--Rˣ has characteristic 2
--This means (1 + u + u²) ∈ Rˣ
--we know (1 + u + u²) ∉ {1, u, u²} (if it was, then the other elements would be each others negative and that is not true)
--So that means (1 + u + u²) ∈ {u³, u⁴}
--consider r = (1 + u + u² + u³ + u⁴), r² = 2(...) + r = r
--if r is a unit, since r² = r, we must have r=1
-- for the two cases of (1 + u + u²) ∈ {u³, u⁴},
-- if (1 + u + u²) = u³ → 2(u³) + u⁴ → 1 = u⁴ contradiction
-- same for (1 + u + u²) = u⁴
sorry
end


#### Eric Rodriguez (Jul 26 2022 at 11:02):

is_cyclic is what is known as a typeclass, so I think that best would be actually to write the first have as haveI, and then obtain the element as obtain ⟨u, hu⟩ := is_cyclic.exists_generator Rˣ so that you can still keep around the cyclic-ness around for other useful lemmas (although it really doesn't seem many exist...)

#### Eric Rodriguez (Jul 26 2022 at 11:02):

THen you can use docs#order_of_eq_card_of_forall_mem_zpowers with your hu to get the order of u

#### Eric Rodriguez (Jul 26 2022 at 11:04):

you can also write your first few lines as  haveI : fact ((5 : ℕ).prime) := ⟨by norm_num⟩, haveI h : is_cyclic Rˣ := is_cyclic_of_prime_card h5u to avoid fiddling with everything!

Last updated: Dec 20 2023 at 11:08 UTC