Using `one_ne_zero`

Stream: new members

[Aniruddh Agarwal]

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]

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

[Johan Commelin]

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]

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

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