# Zulip Chat Archive

## Stream: new members

### Topic: group

#### Amaury Hayat (May 17 2021 at 10:17):

Hi all,

My name is Amaury Hayat, I am a mathematician just beginning with Lean, and I am very happy to join this community! I read the doc and played at the very nice Natural Number Game. I am trying to write some theorems, and I am still struggling with some maths notations in Lean: for instance I am trying to write that for n\in\mathbb{N}^{*}, f : x |-> x^{n} is a group homomorphism from (\mathbb{R}^{*}, \times) in itself and was wondering whether there is already some code to show that (\mathbb{R}^{*}, \times) is a multiplicative group. Thanks a lot in advance, I hope I'll be able to contribute to this project :)

#### Anne Baanen (May 17 2021 at 10:19):

You can write $\mathbb{R}^*$ as `units ℝ`

#### Eric Rodriguez (May 17 2021 at 10:19):

also, you can write LaTeX in Zulip by surrounding it with `$$`

, e.g. $n\in\mathbb{N}^{*}, f : x \mapsto x^{n}$

#### Anne Baanen (May 17 2021 at 10:20):

(Or is $\mathbb{N}^{*}$ something different from the invertible elements, i.e. `{1}`

?)

#### Eric Rodriguez (May 17 2021 at 10:22):

Maybe it's notation for the positive natural numbers? I haven't seen it before either

#### Eric Rodriguez (May 17 2021 at 10:23):

And the fact that it's a group is registered through the type-class system; for example see here for the proof/`instance`

that the units of a monoid (like ℝ) also form a group

#### Eric Rodriguez (May 17 2021 at 10:24):

So you can just start doing group stuff with it and it'll be fine with it

#### Anne Baanen (May 17 2021 at 10:24):

Ah, it's probably `ℕ`

where `*`

is actually addition, so `multiplicative ℕ`

in mathlib

#### Horatiu Cheval (May 17 2021 at 10:28):

I always thought $\mathbb{N}^*$ was a standard notation for the naturals without 0. Maybe it's a regional thing.

#### Mario Carneiro (May 17 2021 at 10:28):

The syntax $R^*$ usually means "without zero", so in this case $\mathbb{N}^*$ means the positive natural numbers `pnat`

. It is also used on other rings like $\mathbb{R}^*$, in which case we are usually interested in the multiplicative structure; this is what $(\mathbb{R}^{*}, \times)$ means (which we would write `units ℝ`

)

#### Riccardo Brasca (May 17 2021 at 10:30):

I had this exact discussion with some friends (they are french and working in analysis). They were shocked that for me $\mathbb{Z}^\ast$ does not mean $\mathbb{Z} \setminus \{0\}$.

#### Mario Carneiro (May 17 2021 at 10:33):

Regarding the question, we already know that `units R`

is an abelian group, so I would generalize this to the statement that `λ x, n • x`

is a group hom on any abelian group

#### Johan Commelin (May 17 2021 at 10:35):

Which as of recently is part of the axioms of (additive) abelian groups

#### Mario Carneiro (May 17 2021 at 10:40):

ah, here it is: docs#gpow.is_group_hom

#### Amaury Hayat (May 17 2021 at 11:50):

Thanks a lot for all these answers ! It's very helpful :) Yes I used $\mathbb{N}^{*}$ for the positive natural numbers, sorry for the confusion I should have remembered that this is just a regional thing.

#### Johan Commelin (May 17 2021 at 11:53):

@Amaury Hayat Confusingly, you need to use `$$`

for inline math on Zulip.

#### Amaury Hayat (May 17 2021 at 12:05):

Ok, thanks ! Seems like I'm a beginner on Zulip as well.

#### Johan Commelin (May 17 2021 at 12:06):

We have all been there (-;

#### Kevin Buzzard (May 17 2021 at 12:51):

Everyone is bikeshedding about $\mathbb{N}^*$ but the statement is true for $\mathbb{N}$ ;-)

@Amaury Hayat here are the two `sorry`

s which Lean would like you to fill in for your result:

```
import data.real.basic
def real.nat_pow_hom (n : ℕ) : units ℝ →* units ℝ :=
{ to_fun := λ u, u^n,
map_one' := begin
sorry
end,
map_mul' := begin
sorry
end }
```

I suspect that there is a way to do it with just one sorry, there should be a constructor for group homs which only demands a proof of `map_mul`

.

#### Amaury Hayat (May 17 2021 at 15:37):

Thanks a lot @Kevin Buzzard for this answer ! Indeed, the statement was conservative. Do you think there would be a way to state it as a theorem (for the sole purpose of exercising in writing statements) like:

```
def f (n: ℕ) (x : units ℝ):=x^n
theorem my_test_th (n : ℕ) : is_group_hom (f n) :=
begin
sorry
end
```

Would this formulation be too naïve (as it implicitly uses that units \br is a group) ? Apologies in advance if this is a silly question: I literally just started writing in Lean this morning.

#### Johan Commelin (May 17 2021 at 16:02):

@Amaury Hayat Yes, some think like that looks fine. Although mathlib no longer uses `is_group_hom`

.

#### Amaury Hayat (May 17 2021 at 16:04):

Great, thanks! I'll use monoid_hom then.

#### Eric Wieser (May 17 2021 at 16:21):

I think we have this in the library as `(powers_mul_hom (units ℝ)).to_monoid_hom.flip n`

(docs#powers_mul_hom)

#### Eric Wieser (May 17 2021 at 16:28):

This also works:

```
import data.real.basic
def real.nat_pow_hom (n : ℕ) : units ℝ →* units ℝ :=
monoid_hom.of (^ n)
```

#### Kevin Buzzard (May 17 2021 at 16:43):

Lean knows that the units of $\R$ (or indeed of any ring) are a group under multiplication -- this "therorem" (as a mathematician would call it), or, more precisely, construction (as Lean would call it), is part of Lean's type class inference system. Eric's proof is just saying "it's in mathlib already" which of course is not surprising.

#### Kevin Buzzard (May 17 2021 at 16:43):

Lean knows that the units of $\R$ (or indeed of any ring) are a group under multiplication -- this "therorem" (as a mathematician would call it), or, more precisely, construction (as Lean would call it), is part of Lean's type class inference system. Eric's proof is just saying "it's in mathlib already" which of course is not surprising.

#### Amaury Hayat (May 17 2021 at 17:38):

Great, thank you for the explanation

Last updated: Dec 20 2023 at 11:08 UTC