Can't find basic lemma

Stream: new members

[Jack J Garzella]

I seem to need the following basic statement, given a [ring α] or [monoid α] or something

example : ∀ h : α, h ∣ f ↔ ∃ j, f = h * j

Though my formulation might be a bit off, library_search doesn't work :(. Does anyone know where I might find this?

[Kevin Buzzard]

In a monoid, there are two notions of division, left division and right division. As far as I know, Lean has neither. Why don't you get your code compiling and working? (by which I mean you should clarify in exactly what generality you need this.) It might be easier to help that way. Lean only has division in commutative situations.

[Jack J Garzella]

Right, whoops. Actually I'm in the context of a polynomial ring polynomial β, but I thought this should hold in more generality, so I tried to state it that way... here is a compiling #mwe

universe u
example {β : Type u} [field β] (f : polynomial β)
  : ∀ h : polynomial β, h ∣ f ↔ ∃ j, f = h * j :=
sorry

[Kevin Buzzard]

oh no it isn't :-)

[Kevin Buzzard]

import data.polynomial
import tactic

universe u
example {β : Type u} [field β] (f : polynomial β)
  : ∀ h : polynomial β, h ∣ f ↔ ∃ j, f = h * j :=
begin
  intro h,
  refl,
end

It's true by definition.

[Kevin Buzzard]

You got lucky -- if you'd done f = j * h it wouldn't have been :-) Sometimes lemmas whose proof is rfl are not explicitly stated in Lean.

[Kevin Buzzard]

Here's how you can investigate these things yourself:

import data.polynomial
import tactic

universe u

#print notation ∣ -- has_dvd.dvd
noncomputable def ZZZ {β : Type u} [field β] : has_dvd (polynomial β) :=
  by apply_instance

#print ZZZ -- comm_semiring_has_dvd

#check @comm_semiring_has_dvd -- dvd is defined for all
-- commutative semirings at least

-- Now right click on `comm_semiring_has_dvd` and go to
-- definition, to see

/-
instance comm_semiring_has_dvd : has_dvd α :=
has_dvd.mk (λ a b, ∃ c, b = a * c)
-/

[Kevin Buzzard]

After the definition is made, there are a ton of lemmas, for example exists_eq_mul_right_of_dvd, dvd.elim, exists_eq_mul_left_of_dvd etc. This is the basic API for dvd, which, as usual in mathlib, is written just after the definition. So once you have located the definition in mathlib (and I sketch how to do this above) this is a neat way to find a bunch of lemmas which you might find useful about the definition. You don't have to worry about reading the proofs -- it's the statements which are the useful things.

[Kevin Buzzard]

\| is notation, has_dvd is the notation typeclass. The by apply_instance incantation is getting the type class inference system to pull out the definition of dvd on the polynomial ring so we can inspect it and find out where it came from.

[Jack J Garzella]

Ok this is super super helpful. I've struggled mightily just to find where implementations of classes like has_dvd, has_one, has_mul, etc. in mathlib.

[Kevin Buzzard]

Once you learn how to ask Lean questions instead of Zulip, you can start processing more quickly. Learning to read error messages is another really useful skill and one that took me quite a while to pick up.

[Scott Morrison]

As long as you remember to read the first, not the last, error, they are surprisingly helpful.