Zulip Chat Archive

Stream: new members

Topic: Can't find basic lemma


Jack J Garzella (Jul 20 2020 at 20:34):

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 (Jul 20 2020 at 20:37):

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 (Jul 21 2020 at 17:06):

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 (Jul 21 2020 at 17:41):

oh no it isn't :-)

Kevin Buzzard (Jul 21 2020 at 17:42):

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 (Jul 21 2020 at 17:44):

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 (Jul 21 2020 at 17:47):

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 (Jul 21 2020 at 17:49):

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 (Jul 21 2020 at 17:51):

\| 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 (Jul 21 2020 at 20:36):

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 (Jul 21 2020 at 20:44):

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 (Jul 21 2020 at 22:43):

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


Last updated: Dec 20 2023 at 11:08 UTC