## Stream: new members

### Topic: coe additive monoid hom

#### Calle Sönne (Mar 16 2019 at 10:33):

I need a theorem that says that coercions from the integers into an additive monoid is an additive monoid homomorphism. I only found the corresponding theorem from the naturals however, is there any for the integers in mathlib?

#### Kenny Lau (Mar 16 2019 at 10:35):

you can't coerce the integers into an additive monoid (where does -1 go to?)

#### Kenny Lau (Mar 16 2019 at 10:35):

import data.int.basic
-- int.cast_add : ∀ {α : Type u_1} [_inst_1 : add_group α] [_inst_2 : has_one α] (m n : ℤ), ↑(m + n) = ↑m + ↑n


#### Calle Sönne (Mar 16 2019 at 10:39):

oh wait I do need is_add_monoid_hom

#### Calle Sönne (Mar 16 2019 at 10:40):

Basically I have this:

{b_1 :
ℕ | a <
finset.sum (finset.range b_1) (λ (x : ℕ), ↑(digit b r x * ↑b ^ (b_1 - 1 - x))) * (↑b ^ b_1)⁻¹} ∈
at_top.sets


and I want to apply sum_hom to move the coercion out of the sum, but this requires that the coercion is an add_monoid_hom

#### Calle Sönne (Mar 16 2019 at 10:41):

is there some other theorem that accomplishes this?

#### Kenny Lau (Mar 16 2019 at 10:42):

import data.int.basic

instance asdf {α : Type*} [add_group α] [has_one α] : is_add_monoid_hom (int.cast : ℤ → α) :=


#### Calle Sönne (Mar 16 2019 at 10:44):

wait now Im confused, how does this work?

#### Kenny Lau (Mar 16 2019 at 10:45):

this tells Lean that int.cast is an add_monoid_hom

#### Calle Sönne (Mar 16 2019 at 10:48):

I was just confused for a second since you said integers cant be mapped into an additive monoid, but I missed that you mapped them into a group.

#### Calle Sönne (Mar 16 2019 at 10:48):

Thank you by the way

#### Kevin Buzzard (Mar 16 2019 at 11:40):

That instance should be in mathlib I guess

#### Johan Commelin (Mar 16 2019 at 12:26):

Isn't there an instance for group homs already? I would expect it to be there....

Last updated: May 13 2021 at 18:26 UTC