is_ideal.neg_iff

Stream: maths

[Patrick Massot]

import ring_theory.ideals

variables {α : Type} [comm_ring α] (N : set α) [is_ideal N]
example (a : α) (h : a ∈ N) : -a ∈ N :=
begin
  -- rwa is_ideal.neg_iff at h,
  rwa @is_ideal.neg_iff _ _ _ N _ at h,
end

Why can't I use the first line?

[Patrick Massot]

Looks like it makes that lemma unusable

[Patrick Massot]

Recall lemma neg_iff {S : set α} [is_ideal S] : a ∈ S ↔ -a ∈ S := ⟨is_submodule.neg, λ h, neg_neg a ▸ is_submodule.neg h⟩

[Chris Hughes]

The set should be explicit. I'm not sure why it happens, but it's the same with rws for is_group_hom, the function that is a group_hom needs to be given explicitly.

[Patrick Massot]

So you suggest modifying the binder in the statement of the lemma?

[Reid Barton]

Maybe it's because a ∈ S is really just S a, that is, a variable function applied to a variable argument. Lean is probably unwilling to try to guess both the function and the argument.

[Kevin Buzzard]

But it shouldn't be unfolding this at all, right?

[Reid Barton]

Yeah that part I am not sure about.