# 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: May 10 2021 at 17:39 UTC