Zulip Chat Archive

Stream: maths

Topic: is_ideal.neg_iff


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

view this post on Zulip Patrick Massot (Oct 06 2018 at 14:15):

Looks like it makes that lemma unusable

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

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

view this post on Zulip Patrick Massot (Oct 06 2018 at 14:20):

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

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

view this post on Zulip Kevin Buzzard (Oct 06 2018 at 14:37):

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

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