# Zulip Chat Archive

## Stream: new members

### Topic: def nat greater than 0

#### Henrik Böving (Apr 18 2021 at 13:51):

Hey, so I'm currently learning lean and I'm trying to formalize a bit of abstract algebra for self learning purposes so i got this class representing a semigroup:

```
class semigroup (H: Type) extends has_mul H :=
(mul_assoc: ∀ (a b c: H), (a * b) * c = a * (b * c))
```

and now I'd basically like to define exponentiation for this class. So I went ahead and wrote

```
def pow {SG: Type*} [semigroup SG] : SG -> nat -> SG
| a (nat.succ 0) := a
| a (nat.succ n) := a * (pow a n)
```

and rightfully so lean does now complain about the fact that I didnt define my pattern for the natural number 0, however this is only possible inside a monoid as far as I'm concerned since a^0 = 1 which is not something I can express inside a semigroup i believe. So my question would be whether there is some way to still formalize what i want by basically saying that this function only works for "any nat greater than 0"? Or do i have to give up defining this function for a semigroup and instead use a monoid?

#### Eric Wieser (Apr 18 2021 at 13:58):

You could use docs#pnat (`ℕ+`

) instead of nat

#### Henrik Böving (Apr 18 2021 at 13:59):

Looks just like what I needed, thank you!

#### Henrik Böving (Apr 18 2021 at 14:13):

So I now ended up with

```
def pow {SG: Type*} [half_group SG] : SG -> pnat -> SG
| a one := a
| a (pnat.succ n) := a * (pow a n)
```

but pnat.succ isn't actually defined...and I can't use nat.succ anymore either. Any idea on what the correct notation for this would be?

#### Eric Wieser (Apr 18 2021 at 14:54):

This works:

```
import data.pnat.basic
namespace henrik
class semigroup (H: Type) extends has_mul H :=
(mul_assoc: ∀ (a b c: H), (a * b) * c = a * (b * c))
def pow {SG: Type*} [semigroup SG] : SG -> pnat -> SG
| a ⟨0, h⟩ := false.elim (nat.lt_asymm h h)
| a ⟨1, h⟩ := a
| a ⟨n + 2, h⟩ :=
have n.succ < n + 2 := nat.succ_le_succ rfl.le,
a * (pow a ⟨n.succ, n.zero_lt_succ⟩)
end henrik
```

Last updated: Dec 20 2023 at 11:08 UTC