Zulip Chat Archive

Stream: maths

Topic: division ring to nontrivial semiring


view this post on Zulip Kenny Lau (Jul 30 2020 at 06:57):

is every semiring homomorphism from a division ring to a nontrivial semiring injective?

view this post on Zulip Kenny Lau (Jul 30 2020 at 07:08):

never mind I proved it

view this post on Zulip Yury G. Kudryashov (Jul 30 2020 at 07:50):

Actually docs@monoid_hom.map_ne_zero works if the codomain is a [monoid_with_zero] + [nontrivial].

view this post on Zulip Kenny Lau (Jul 30 2020 at 07:52):

it's in my upcoming PR

view this post on Zulip Yury G. Kudryashov (Jul 30 2020 at 08:02):

Sorry, I created a branch before reading your reply. Do you prefer to merge my fixes with yours, or to have 2 PRs?

view this post on Zulip Yury G. Kudryashov (Jul 30 2020 at 08:03):

I also removed comm_ assumption from map_units_inv.

view this post on Zulip Kenny Lau (Jul 30 2020 at 08:11):

go ahead and PR it then

view this post on Zulip Yury G. Kudryashov (Jul 30 2020 at 08:20):

Do you have monoid_hom.injective_iff for a homomorphism from a group to a monoid?

view this post on Zulip Kenny Lau (Jul 30 2020 at 08:25):

yes

view this post on Zulip Kenny Lau (Jul 30 2020 at 08:25):

go ahead and PR it, my PR will be much larger, so I'll just merge mathlib after your PR

view this post on Zulip Yury G. Kudryashov (Jul 30 2020 at 08:32):

#3630


Last updated: May 10 2021 at 08:14 UTC