## Stream: new members

### Topic: Using one_ne_zero

#### Aniruddh Agarwal (Jun 30 2020 at 18:42):

I'm trying to use one_ne_zero as follows:

import algebra.associated
import algebra.group_power
import ring_theory.ideal_operations
import ring_theory.ideals

variables {α : Type*} [comm_ring α]

open_locale classical

/- An element a of a ring α is a zero divisor if there exists a b ∈ α
such that b ≠ 0 and ab = 0. -/
def is_zero_divisor [comm_ring α] (a : α)
:= ∃ b : α, b ≠ (0 : α) ∧ a * b = (0 : α)

/- Zero is a zero divisor in a nonzero ring. -/
theorem zero_zero_divisor_in_nz_ring [nonzero_comm_ring α]
: is_zero_divisor (0 : α) :=
begin
use 1,
split,
{ exact one_ne_zero },
{ sorry }
end


but lean is complaining:

invalid type ascription, term has type
@ne ?m_1 1 0
but is expected to have type
@ne α 1 0
state:
α : Type u_1,
_inst_1 : comm_ring α,
_inst_2 : nonzero_comm_ring α
⊢ 1 ≠ 0 (lean-checker)


anybody know what's up?

#### Yakov Pechersky (Jun 30 2020 at 18:43):

You have two different instances of comm_ring for \a. Maybe you want to say [nonzero \a]?

#### Johan Commelin (Jun 30 2020 at 18:44):

nonzero_comm_ring \a doesn't exist anymore. Kenny removed it one or two weeks ago. Are you working with a (slightly) older mathlib?

#### Johan Commelin (Jun 30 2020 at 18:45):

@Aniruddh Agarwal Note that you have the same problem in your definition of zero divisor. It's just not showing up... but you still have two ring instances there.

#### Aniruddh Agarwal (Jun 30 2020 at 18:47):

Yeah, I was working with an older mathlib. Let me try Yakov's suggestion after upgrading it

Last updated: May 13 2021 at 17:42 UTC