# Zulip Chat Archive

## 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`

,

- Is there a way I can use this to refer to all the units as powers of
`u`

? where`1 = u^5`

- 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