# 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 $G$ where $\forall x,y \in G, \exists z \in G$ such that $x*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: May 17 2021 at 23:14 UTC