Zulip Chat Archive

Stream: new members

Topic: coe additive monoid hom


view this post on Zulip 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?

view this post on Zulip Kenny Lau (Mar 16 2019 at 10:35):

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

view this post on Zulip Kenny Lau (Mar 16 2019 at 10:35):

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

view this post on Zulip Calle Sönne (Mar 16 2019 at 10:36):

ah, so I should look for add_group_hom instead?

view this post on Zulip Calle Sönne (Mar 16 2019 at 10:39):

oh wait I do need is_add_monoid_hom

view this post on Zulip 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

view this post on Zulip Calle Sönne (Mar 16 2019 at 10:41):

is there some other theorem that accomplishes this?

view this post on Zulip 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 :   α) :=
int.cast_zero, int.cast_add

view this post on Zulip Calle Sönne (Mar 16 2019 at 10:44):

wait now Im confused, how does this work?

view this post on Zulip Kenny Lau (Mar 16 2019 at 10:45):

this tells Lean that int.cast is an add_monoid_hom

view this post on Zulip 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.

view this post on Zulip Calle Sönne (Mar 16 2019 at 10:48):

Thank you by the way

view this post on Zulip Kevin Buzzard (Mar 16 2019 at 11:40):

That instance should be in mathlib I guess

view this post on Zulip 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