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: Dec 20 2023 at 11:08 UTC