# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: Is there a `ring` instance on a semiring that is a ℤ-alge...

#### Damiano Testa (Mar 03 2021 at 04:17):

Dear All,

after the major breakdown that my last attempt with `instances`

caused, I am a little worried about this one. Is there a `ring`

instance on a semiring that is a ℤ-algebra?

In the code below, replacing the instances with `by apply_instance`

does not work. Also, I imagine that there are easier proofs of the unique fact that this instance requires.

Thanks!

```
import algebra.algebra.basic
variables (S : Type*) [semiring S] [algebra ℤ S]
instance negZ : has_neg S := ⟨λ r, (- 1 : ℤ) • r⟩
instance Zalg.to_ring : ring S :=
{ neg := has_neg.neg,
add_left_neg := λ a, begin
simp [(has_neg.neg)],
nth_rewrite 1 ← one_smul ℤ a,
rw ← add_smul,
have : (int.neg 1 + 1) = 0,
{ change ((- 1 : ℤ) + 1 = 0),
exact neg_add_self _ },
rw [this, zero_smul],
end,
..(infer_instance : semiring S) }
```

#### Damiano Testa (Mar 03 2021 at 04:28):

In fact, instead of ℤ, you could get the proof to work for a general `comm_ring`

, instead:

```
variables (R S : Type*) [comm_ring R] [semiring S] [algebra R S]
instance negZ : has_neg S := ⟨λ r, (- 1 : R) • r⟩
instance Zalg.to_ring : ring S :=
{ neg := λ r, (- 1 : R) • r,
add_left_neg := λ a, begin
simp [(has_neg.neg)],
nth_rewrite 1 ← one_smul R a,
rw ← add_smul,
have : (sub_neg_monoid.neg (1 : ℤ) • (1 : R) + 1) = 0,
{ change ((- 1 : R) + 1 = 0),
convert neg_add_self (1 : R),
simpa [negZ], },
rw [this, zero_smul],
end,
..(infer_instance : semiring S) }
```

#### Adam Topaz (Mar 03 2021 at 04:31):

Yeah this was an issue that came up a while ago. @Eric Wieser do you remember how this ended up?

#### Damiano Testa (Mar 03 2021 at 04:36):

I am worried that this might cause more trouble than the whole "subsets of semirings closed under addition and multiplication are semirings" mess. (PR #6489 et al)

#### Eric Wieser (Mar 03 2021 at 06:50):

Was it docs#algebra.semiring_to_ring?

#### Eric Wieser (Mar 03 2021 at 06:51):

Which isn't safe to use unless you know `A`

and know you will be the only one to give it a ring instance

#### Damiano Testa (Mar 03 2021 at 08:40):

Thanks, this looks exactly what I was looking for! I will try to use it with care!

#### Eric Wieser (Mar 03 2021 at 08:42):

docs#semimodule.add_comm_monoid_to_add_comm_group is similar

#### Damiano Testa (Mar 03 2021 at 08:47):

Great, thanks! I may indeed want to convert between (semi)modules, when acquiring/losing subtractions!

Last updated: May 17 2021 at 14:12 UTC