List of group elements using types

Stream: new members

[Daniel Eriksson]

Hello, I am Daniel, a PhD student at KTH working in PDEs. I am taking a Lean course where we have been following MIL. As a small step in formalizing a proof using group actions for Cauchy theorem, I am trying to construct a list of group elements using types. I have tried using variables with (), {} and putting G in the definition, but either it has wrong type or Lean cannot synthesize the implicit argument.

import MIL.Common
variable {G : Type*} [Group G] [Finite G] {g₁:G}
def lg: List G := [g₁, g₁, g₁]

def Z:={l:List G // l.length = 3}

def z:Z := ⟨lg,rfl⟩ -- don't know how to synthesize implicit argument 'G'

variable (G : Type*) [Group G] [Finite G] {g₁:G}

def lg: List G := [g₁, g₁, g₁]

def Z:={l:List G // l.length = 3}

def z:Z G := ⟨lg,rfl⟩ -- argument lg has type (G : Type ?u.116) → {g₁ : G} → List G : Type (?u.116 + 1) but is expected to have type List G : Type u_1

For a list of Finset Nat I could do it, but this is trickier as Z depends on G.
How can I do this?

[Yaël Dillies]

Here's a suggestion for how to do things:

variable {G : Type*} [Group G] [Finite G] {g₁ : G}

variable (g₁) in
def lg : List G := [g₁, g₁, g₁]

variable (G) in
def Z := {l : List G // l.length = 3}

variable (g₁) in
def z : Z G := ⟨lg g₁, rfl⟩

[Daniel Eriksson]

Nice, some playing around with declaring variables, thanks!