# Zulip Chat Archive

## Stream: new members

### Topic: has_zero equality

#### Duckki Oe (Oct 22 2020 at 06:52):

How do you prove this?

α: Type

_inst_5: has_zero α

⊢ mul_zero_class.to_has_zero α = _inst_5

#### Johan Commelin (Oct 22 2020 at 06:54):

It might not be provable

#### Johan Commelin (Oct 22 2020 at 06:54):

If you have to unrelated instances of `has_zero`

, they will be actually different.

#### Johan Commelin (Oct 22 2020 at 06:55):

So we need more context.

#### Johan Commelin (Oct 22 2020 at 06:56):

I could be evil and write

```
instance evil_zero : has_zero nat := { zero := 1 }
```

Now you certainly cannot prove `evil_zero = nat.has_zero`

, even though both have type `has_zero nat`

.

#### Jalex Stark (Oct 22 2020 at 13:10):

by the way format your code using #backticks

#### Duckki Oe (Oct 22 2020 at 16:29):

I'm trying to prove this:

```
section std_basis
open matrix
variables {m n: Type*} [fintype m] [fintype n]
variables [decidable_eq m] [decidable_eq n]
variables {α : Type} [has_zero α] [semiring α]
example {i' : m} {j' : n} {v : α}
: ∀ {i j}, ¬ i = i' ∨ ¬ j = j' → std_basis_matrix i' j' v i j = 0
:= begin
intros i j h,
unfold std_basis_matrix,
rwa if_neg, {
sorry
}
end
```

The zero from std_basis_matrix is not an instance of `has_zero α`

, instead it seems to be `mul_zero_class.to_has_zero α`

.

#### Mario Carneiro (Oct 22 2020 at 16:30):

`[has_zero α] [semiring α]`

This is bad, you just put two zeros on `α`

#### Mario Carneiro (Oct 22 2020 at 16:31):

The error you are getting is because you need one zero and have the other

#### Mario Carneiro (Oct 22 2020 at 16:32):

you should just delete `[has_zero α]`

and it should work

#### Duckki Oe (Oct 22 2020 at 16:37):

That was it. Thanks! @Mario Carneiro

Last updated: May 14 2021 at 07:19 UTC