Zulip Chat Archive

Stream: new members

Topic: Defining Properties of a Semigroup

Adam Dionne (Nov 15 2020 at 03:49):

Hello, I am new to Lean and am trying to solve some problems. I am working with a commutative semigroup GG where x,yG,zG\forall x,y \in G, \exists z \in G such that xz=yx*z=y. So I want to define this to be true, and I've tried

import algebra.group.defs

universe u

variables {G: Type u}[comm_semigroup G]

def semigroupA : G :=  x y : G,  z : G, x*y = z

This gives me the error

type mismatch, term
   (x y : G),  (z : G), x * y = z
has type
  Prop : Type
but is expected to have type
  G : Type u

Which I am having trouble interpreting, and with a lot of Googling I haven't had any luck. Any help would be greatly appreciated!

Alex J. Best (Nov 15 2020 at 03:57):

If you want to assume that your semigroup satisfies that property you can add a hypothesis as a variable

variable (h_div :  x y : G,  z : G, x*y = z)

Alex J. Best (Nov 15 2020 at 03:58):

If you want to give a name to this property you can define a proposition

def is_divisible (G : Type*) [comm_semigroup G] : Prop :=  x y : G,  z : G, x*y = z

Kevin Buzzard (Nov 15 2020 at 08:56):

The error means "you told me that semigroupA was going to be a term of type G because you wrote : G but then when you wrote the definition after the := it turned out to be a true-false statement. This doesn't add up"

Last updated: Dec 20 2023 at 11:08 UTC