Zulip Chat Archive

Stream: maths

Topic: division ring to nontrivial semiring

Kenny Lau (Jul 30 2020 at 06:57):

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

Kenny Lau (Jul 30 2020 at 07:08):

never mind I proved it

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].

Kenny Lau (Jul 30 2020 at 07:52):

it's in my upcoming PR

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?

Yury G. Kudryashov (Jul 30 2020 at 08:03):

I also removed comm_ assumption from map_units_inv.

Kenny Lau (Jul 30 2020 at 08:11):

go ahead and PR it then

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?

Kenny Lau (Jul 30 2020 at 08:25):

yes

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

Yury G. Kudryashov (Jul 30 2020 at 08:32):

#3630

Last updated: Dec 20 2023 at 11:08 UTC