## 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