Additive coercions

Stream: Is there code for X?

[Ashvni Narayanan]

I want to define a coercion from ℚ to a ring R which is additive, that is , something to this effect :

example (n : ℕ) [has_coe ℚ R] (coe : ℚ →+ R) {s : finset (zmod n)} {f : (zmod n) → ℚ} :
  ∑ a in s, ((f a) : R) = ↑(∑ a in s, (f a)) :=

Here any space works in place of zmod n (I think). Is there something I am missing? I think using rat.cast_add should do it, but I am not sure.
Any help is appreciated, thank you!

[Yakov Pechersky]

Do you want to define a coercion, or given such a coercion which is an add_hom, prove that lemma?

[Kevin Buzzard]

guessing docs#finset.sum_coe or docs#finset.coe_sum ? Nope...

[Kevin Buzzard]

Hmm I guess I see why not -- how does one say that the coercion is a monoid hom? We do have docs#add_monoid_hom.finset_sum_apply though -- maybe that helps

[Ashvni Narayanan]

Yakov Pechersky said:

Do you want to define a coercion, or given such a coercion which is an add_hom, prove that lemma?

I think I would like to use the canonical rat.cast.

[Yakov Pechersky]

If I understand correctly, rat.cast casts a rat into a division_ring. Is that the case for R here?

[Yakov Pechersky]

import data.zmod.basic

variables {R : Type*} [ring R] [has_coe ℚ R]

open_locale big_operators

example {n : ℕ} (s : finset (zmod n)) (f : (zmod n) → ℚ) {coe' : ℚ →+ R}
  (h : ∀ q : ℚ, (q : R) = coe' q) :
  ∑ a in s, ((f a) : R) = ↑(∑ a in s, (f a)) :=
by simpa [h] using (coe'.map_sum f s).symm

[Yakov Pechersky]

That's a #mwe, with more proper argument explicit/implicit style, and the crucial hypothesis you need to prove, which I called h.

[Ashvni Narayanan]

Yakov Pechersky said:

import data.zmod.basic

variables {R : Type*} [ring R] [has_coe ℚ R]

open_locale big_operators

example {n : ℕ} (s : finset (zmod n)) (f : (zmod n) → ℚ) {coe' : ℚ →+ R}
  (h : ∀ q : ℚ, (q : R) = coe' q) :
  ∑ a in s, ((f a) : R) = ↑(∑ a in s, (f a)) :=
by simpa [h] using (coe'.map_sum f s).symm

This is helpful, thank you!