Stream: new members

Topic: mul_div_comm

James Arthur (Jun 25 2020 at 18:36):

Hello, I'm trying to do something I plucked out of my LA textbook. I'm slowly working through it... here is the code I have:

example (a b : ℝ) (fa : a ≠ 0) (fb : b ≠ 0) : ∀ a, ∃ b, a*b = 1 :=
begin
intro a,
use (1/a),
rw mul_div_comm,

end


Aparently mul_div_comm is on a group that includes the naturals? Is there a thing in mathlib that just allows me to do:

a * (b/c)  to b * (a/c)


Patrick Massot (Jun 25 2020 at 18:38):

This is not what you wanted to state.

Patrick Massot (Jun 25 2020 at 18:40):

Hint: after the intro line, you probably have two a in your context.

Aniruddh Agarwal (Jun 25 2020 at 18:43):

Also, try use (a⁻¹) instead of use (1/a). (You can type a⁻¹ by typing "a\inv")

James Arthur (Jun 25 2020 at 18:44):

So it's to do with:

(a b : ℝ) (fa : a ≠ 0) (fb : b ≠ 0) : ∀ a, ∃ b, a*b = 1


Johan Commelin (Jun 25 2020 at 18:44):

Patrick is trying to make you turn the first line into

example (a : ℝ) (fa : a ≠ 0) : ∃ b, a*b = 1 :=


Johan Commelin (Jun 25 2020 at 18:44):

Can you understand the difference, and why it matters?

James Arthur (Jun 25 2020 at 18:45):

So does Lean already know I want it to be for all a? I knew fb was superfluous

Johan Commelin (Jun 25 2020 at 18:46):

Yup, having something left of the : means forall

Aniruddh Agarwal (Jun 25 2020 at 18:46):

Note that what Johan wrote is equivalent to:

example : ∀ a : ℝ, a ≠ 0 → ∃ b, a*b = 1 :=


James Arthur (Jun 25 2020 at 18:48):

Thankyou!!

Last updated: Dec 20 2023 at 11:08 UTC