Zulip Chat Archive

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 : α) :=
use 1,
{ exact one_ne_zero },
{ sorry }

but lean is complaining:

invalid type ascription, term has type
   @ne ?m_1 1 0
 but is expected to have type
   @ne α 1 0
 α : 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: Dec 20 2023 at 11:08 UTC