injectivity of multiplication on EReal

Stream: Is there code for X?

[Ruben Van de Velde]

Do we really not have either of these?

lemma mul_right_inj {a b c : EReal} (hbot : b ≠ ⊥) (htop : b ≠ ⊤) (hzero : b ≠ 0) : a * b = c * b ↔ a = c := sorry
lemma mul_right_coe_inj {a c : EReal} {b : ℝ} (hzero : b ≠ 0) : a * b = c * b ↔ a = c := sorry

(I have an ugly proof in #20293)

[Edward van de Meent]

from the looks of it, no... but i'm also pretty sure these'd be called something like mul_left_cancel or something like that

[Edward van de Meent]

see for example docs#mul_left_cancel

[Ruben Van de Velde]

mul_left_cancel is the implication; this is the iff. Though that would be fine as well

[Damiano Testa]

Also the analogous ones for ENNReal appear to be missing.

[Damiano Testa]

Maybe the ENNReal ones exist docs#ENNReal.mul_eq_mul_left ?

[Ruben Van de Velde]

Damiano Testa said:

Maybe the ENNReal ones exist docs#ENNReal.mul_eq_mul_left ?

I'll rename those, thanks for the pointer

[Ruben Van de Velde]

#20880