Stream: maths

Topic: is_ideal.neg_iff

Patrick Massot (Oct 06 2018 at 14:15):

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 (Oct 06 2018 at 14:15):

Looks like it makes that lemma unusable

Patrick Massot (Oct 06 2018 at 14:16):

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 (Oct 06 2018 at 14:17):

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 (Oct 06 2018 at 14:20):

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

Reid Barton (Oct 06 2018 at 14:36):

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 (Oct 06 2018 at 14:37):

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

Reid Barton (Oct 06 2018 at 14:37):

Yeah that part I am not sure about.

Last updated: May 12 2021 at 08:14 UTC