coe additive monoid hom

Stream: new members

[Calle Sönne]

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]

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

[Kenny Lau]

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

[Calle Sönne]

ah, so I should look for add_group_hom instead?

[Calle Sönne]

oh wait I do need is_add_monoid_hom

[Calle Sönne]

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]

is there some other theorem that accomplishes this?

[Kenny Lau]

import data.int.basic

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

[Calle Sönne]

wait now Im confused, how does this work?

[Kenny Lau]

this tells Lean that int.cast is an add_monoid_hom

[Calle Sönne]

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]

Thank you by the way

[Kevin Buzzard]

That instance should be in mathlib I guess

[Johan Commelin]

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