mul_div_comm

Stream: new members

[James Arthur]

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]

This is not what you wanted to state.

[Patrick Massot]

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

[Aniruddh Agarwal]

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

[James Arthur]

So it's to do with:

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

[Johan Commelin]

Patrick is trying to make you turn the first line into

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

[Johan Commelin]

Can you understand the difference, and why it matters?

[James Arthur]

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

[Johan Commelin]

Yup, having something left of the : means forall

[Aniruddh Agarwal]

Note that what Johan wrote is equivalent to:

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

[James Arthur]

Thankyou!!