Algebra map is injective

Stream: Is there code for X?

[Thomas Browning]

What's the best way to prove function.injective (algebra_map ℤ ℂ)? Judging by some old code I had lying around, it seems like int.cast_injective used to work, but now it looks like algebra_map ℤ ℂ is not defeq to coe.

[Alex J. Best]

import data.complex.basic
lemma hi : function.injective (algebra_map ℤ ℂ) := int.cast_injective
#print hi

works for me in the web editor

[Eric Wieser]

There are multiple non-defeq z-algebra instances

[Eric Wieser]

Which one you get depends on your imports along with other things

[Eric Wieser]

by convert int.cast_injective should work

[Eric Wieser]

I think adding add_comm_monoid.of_nat and add_comm_group.of_int would fix this.

[Eric Wieser]

(this is in the future work section of my FMM 2021 paper)