Zulip Chat Archive

Stream: new members

Topic: Using `one_ne_zero`


view this post on Zulip 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?

view this post on Zulip 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]?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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