Associated abs

Stream: Is there code for X?

[Xavier Roblot]

I don't think we have the following

import Mathlib

theorem associated_abs {α : Type*} [Ring α] [LinearOrder α] (x : α) :
    Associated x |x| := by
  obtain h | h := abs_choice x
  · rw [h]
  · rw [h]
    exact ⟨-1, by simp⟩

Somehow I also have the feeling that the hypothesis are too strong but I haven't been able to generalize it. Also I have a hard time figuring out where to put it

[Riccardo Brasca]

Looking at find_home! I think Mathlib.Algebra.Ring.Divisibility.Lemmas is a reasonable place.

[Riccardo Brasca]

If you add it, can you add to Mathlib.RingTheory.Ideal.Span the corollary that they generate the same ideal?

[Xavier Roblot]

Riccardo Brasca said:

If you add it, can you add to Mathlib.RingTheory.Ideal.Span the corollary that they generate the same ideal?

That's my plan :wink:

[Riccardo Brasca]

Ahah, I guess you need it for p.natAbs or something similar :D

[Riccardo Brasca]

Anyway we surely have that -x and x are associated

[Xavier Roblot]

Riccardo Brasca said:

Anyway we surely have that -x and x are associated

exact? does not find it

[Riccardo Brasca]

Associated.neg_left

[Andrew Yang]

(btw does import Mathlib.lean work?)

[Riccardo Brasca]

with Associated.rfl

[Riccardo Brasca]

Andrew Yang said:

(btw does import Mathlib.lean work?)

No

[Riccardo Brasca]

And since you are at it, Associated.rfl and Associated.refl are identical.

[Xavier Roblot]

Oh, I fixed that. Sorry

[Andrew Yang]

Riccardo Brasca said:

And since you are at it, Associated.rfl and Associated.refl are identical.

refl has x explicit and rfl has x implicit. I think this is a universal (though maybe not well-documented) naming convention.

[Riccardo Brasca]

ah sorry, you're right

[Xavier Roblot]

Riccardo Brasca said:

Associated.neg_left

That does not say exactly that x and -x are associated, so I think it is worth adding that result too.

[Xavier Roblot]

Riccardo Brasca said:

Ahah, I guess you need it for p.natAbs or something similar :smile:

I need it to prove that the norm of an ideal of Z is a generator of that ideal.

[Andrew Yang]

Is this in #21950 useful to you?

[Andrew Yang]

Probably the otherway around. If you can prove that then I can have a better map in my PR.

[Xavier Roblot]

I am away from my computer for the moment but I'll do that soon

[Xavier Roblot]

#24933

[Eric Wieser]

Xavier Roblot said:

That does not say exactly that x and -x are associated, so I think it is worth adding that result too.

as I claim in the Pr, I think it's not worth adding; we don't have the analogous result for Commute

[Eric Wieser]

Adding it just makes naming things hard

[Filippo A. E. Nuccio]

Pinging @Salvatore Mercuri who has been thinking about this as well.