Zulip Chat Archive
Stream: mathlib4
Topic: RingHom.toIntAlgHom
Daniel Weber (Sep 13 2024 at 16:52):
Why does docs#RingHom.toIntAlgHom take [Algebra ℤ R] [Algebra ℤ S] instead of inferring them from the Ring instances?
Eric Wieser (Sep 13 2024 at 17:03):
I think this might predate us fixing the diamonds
Eric Wieser (Sep 13 2024 at 17:04):
It's especially strange that the Nat version doesn't do the same thing!
Daniel Weber (Sep 14 2024 at 03:31):
this is removed in #16790
Last updated: May 02 2025 at 03:31 UTC