Ideal.mul_le_left

Stream: mathlib4

[Kevin Buzzard]

Should docs#Ideal.mul_le_left be called Ideal.mul_le_right or is this just another twist in the naming convention which I don't understand?

[Ruben Van de Velde]

left_mul_le? I never can tell left and right apart anyway

[Kevin Buzzard]

I found this when adding some lemmas to #13308 at Andrew Yang's suggestion. He wanted quotientMulEquivQuotientProd_fst analogous to quotientInfEquivQuotientProd_fst so I cut and pasted the proof, changing all I ⊓ Js to I * Js and the only problem was that inf_le_left needed to be changed to mul_le_right :-) (see docs#inf_le_left ).

[Kevin Buzzard]

Related: it's great that we have docs#inf_le_left and docs#inf_le_left' so you can decide whether you want it to be a simp lemma or not. What the heck is going on there??

[Ruben Van de Velde]

mathlib3 had:

@[simp] theorem inf_le_left : a ⊓ b ≤ a :=
semilattice_inf.inf_le_left a b

@[ematch] theorem inf_le_left' : (: a ⊓ b :) ≤ a :=
semilattice_inf.inf_le_left a b

[Ruben Van de Velde]

Presumably the ematch did something there, and it no longer does in lean

[Kevin Buzzard]

Is it possible to write some meta code which looks through the library trying to spot all pairs of distinct declarations which are syntactically equal?

[Kevin Buzzard]

(I guess the answer is inevitably "yes" -- perhaps more interesting is "...and which terminates in finite time?"

[Ruben Van de Velde]

#13513

[Ruben Van de Velde]

And finite time for a mathematician or a physicist?

[Yaël Dillies]

Kevin Buzzard said:

Should docs#Ideal.mul_le_left be called Ideal.mul_le_right

Yes.

[Kim Morrison]

Kevin Buzzard said:

(I guess the answer is inevitably "yes" -- perhaps more interesting is "...and which terminates in finite time?"

I think it should be pretty okay. Shove things into a DiscrTree, and then check candidate collisions by hand.