Dealing with finite set of units of a ring

Stream: new members

[Jamie Reason]

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]

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]

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

[Eric Rodriguez]

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!