Defining Properties of a Semigroup

Stream: new members

[Adam Dionne]

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]

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]

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]

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"