Zulip Chat Archive
Stream: Is there code for X?
Topic: ENNReal.mul_div
Eric Rodriguez (Jun 20 2023 at 08:11):
theorem ENNReal.mul_div (a b c : ℝ≥0∞) : a * (b / c) = (a * b) / c := sorry
I can't seem to find it anywhere!
Eric Wieser (Jun 20 2023 at 08:16):
simp_rw [div_eq_mul_inv, mul_assoc]?
Eric Rodriguez (Jun 20 2023 at 08:18):
ennreal is not a div_inv_monoid but docs#ennreal.div_eq_inv_mul so I guess this can work
Eric Rodriguez (Jun 20 2023 at 08:18):
give me a sec
Eric Rodriguez (Jun 20 2023 at 08:20):
by simp only [ENNReal.div_eq_inv_mul, mul_left_comm] works. thanks!
Eric Wieser (Jun 20 2023 at 08:26):
Why is it not a div_inv_monoid?
Eric Wieser (Jun 20 2023 at 08:26):
it's a monoid, right?
Kevin Buzzard (Jun 20 2023 at 08:29):
Mathematically it's not a monoid because 0 * infinity can't be given a meaningful answer. With junk values it may or may not be a Lean monoid.
Eric Wieser (Jun 20 2023 at 08:30):
Since when did monoids have a 0?
Kevin Buzzard (Jun 20 2023 at 08:30):
I'm talking about ENNReal
Eric Wieser (Jun 20 2023 at 08:30):
docs#ennreal.linear_ordered_comm_monoid_with_zero
Kevin Buzzard (Jun 20 2023 at 08:30):
and I'm saying that it's not obvious that multiplication is associative, this would need to be checked because 0 * infinity * 0 is "random junk value"
Eric Wieser (Jun 20 2023 at 08:31):
I think the solution to this thread is to add the div_inv_monoid instance
Eric Wieser (Jun 20 2023 at 08:31):
docs#mul_div should then apply
Kevin Buzzard (Jun 20 2023 at 08:31):
You might find that someone else wants 0^{-1}=infty not 0
Kevin Buzzard (Jun 20 2023 at 08:32):
I think this has come up before
Eric Wieser (Jun 20 2023 at 08:32):
That's good, because docs#ennreal.inv_zero is already that statement IIRC?
Eric Wieser (Jun 20 2023 at 08:33):
div_inv_monoid doesn't require inv 0 = 0
Eric Wieser (Jun 20 2023 at 08:33):
All it means is "there is some random inverse that extends to division and to a power operation
Eric Wieser (Jun 20 2023 at 08:34):
Maybe the power operation is trouble
Kevin Buzzard (Jun 20 2023 at 08:34):
oh then maybe you're OK! But if so then I'm surprised Yael didn't PR this instance months ago
Kevin Buzzard (Jun 20 2023 at 08:34):
I have it in my head that there's an obstruction, I've just guessed wrong twice so far
Eric Wieser (Jun 20 2023 at 08:41):
Eric Wieser (Jun 20 2023 at 08:41):
So the answer to this thread is docs#mul_div
Eric Wieser (Jun 20 2023 at 08:44):
Huh, the definition of docs#ennreal.has_inv is pretty surprising. I expected a definition by cases
Kevin Buzzard (Jun 20 2023 at 08:52):
It's been specially obfuscated to confuse computer scientists.
Yaël Dillies (Jun 20 2023 at 10:26):
Sorry yes that's right. mul_div will work here, although we're missing a lot of related lemmas. I'm adding a few of them in #19199.
Eric Rodriguez (Jun 20 2023 at 17:02):
I remember it not working, but maybe it was so late in the morning I just missed that the brackets were misplaced
Yury G. Kudryashov (Jun 21 2023 at 00:21):
div_eq_inv_mul doesn't work for ENNReal because we don't have DivInvCommMonoid.
Yury G. Kudryashov (Jun 21 2023 at 00:22):
(I mean, doesn't work automatically)
Yury G. Kudryashov (Jun 21 2023 at 00:24):
Eric Wieser said:
Huh, the definition of docs#ennreal.has_inv is pretty surprising. I expected a definition by cases
I think that we should redefine it by cases so that at least ENNReal.inv_top becomes rfl but this should wait for a month or two.
Eric Rodriguez (Jun 21 2023 at 09:16):
Eric Rodriguez said:
I remember it not working, but maybe it was so late in the morning I just missed that the brackets were misplaced
so I remember what this was, exact? didn't find it. but that just happens sometimes
Eric Rodriguez (Jun 21 2023 at 09:17):
I've made a tracking issue for this, Yury. !4#5339
Last updated: Dec 20 2023 at 11:08 UTC