Zulip Chat Archive

Stream: general

Topic: real.mul_inv


Bolton Bailey (Dec 23 2021 at 00:18):

I spent some time looking for the lemma (a * b)⁻¹ = a⁻¹ * b⁻¹ for reals. I eventually found mul_inv₀, but it seems like this would be hard for someone to guess, or find in the docs. Can we make real.mul_inv an alias for the real version of this lemma?

Eric Rodriguez (Dec 23 2021 at 00:19):

I think this is pretty sensible; mul_inv for groups, mul_inv₀ for groups with zero [like (R,*)]. I feel like it's surprising the first time but thenforth fine. Maybe in undergraduate mode...

Heather Macbeth (Dec 23 2021 at 00:32):

I don't think we should provide aliases of a lemma about a typeclass for every instance of that typeclass. That's what library_search is for.

import data.real.basic

example (a b : ) : (a * b)⁻¹ = a⁻¹ * b⁻¹ := by library_search

Heather Macbeth (Dec 23 2021 at 00:32):

More generally, do you know about the automation we have for such things, like ring and field_simp?

Bolton Bailey (Dec 23 2021 at 00:47):

Yes I know about the automation, but in my case, ring and field_simp failed to resolve or make noticeable progress on the goal.
I suppose I could have tried library_search. I guess the reason I didn't here is that I decided that if the lemma existed, I would probably be able to find it by searching "mul inv" in the docs, but I did that and didn't find it. Then I went to the definition of group_with_zero in algebra/group_with_zero/defs.lean and didn't find it nearby, then later realized that what I needed was in algebra/group_with_zero/basic.lean.

Bolton Bailey (Dec 23 2021 at 00:48):

I just felt my confusion would have been avoided if this lemma, which is identical to mul_inv, had the same name.

Bolton Bailey (Dec 23 2021 at 00:56):

Perhaps I don't know as much about the proof automation as I think. Is there a single-tactic or two-tactic proof of the following lemma:

import data.real.basic
lemma equality4 {x : } (h : x  0) : 2 * x / 3 * log 4 / (x * log 4) = 2 / 3 :=
begin
  sorry,
end

Heather Macbeth (Dec 23 2021 at 00:59):

import analysis.special_functions.log

open real

lemma equality4 {x : } (h : x  0) : 2 * x / 3 * log 4 / (x * log 4) = 2 / 3 :=
begin
  have : log 4  0 := real.log_ne_zero_of_pos_of_ne_one (by norm_num) (by norm_num),
  field_simp,
  ring
end

Last updated: Dec 20 2023 at 11:08 UTC