## 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 ℝ

#### 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 sorrys 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