## Stream: new members

### Topic: Using div_self

#### Eric Wieser (Jun 17 2020 at 14:53):

Having some difficulty applying div_self to a trivial goal:

type mismatch at application
div_self h2
term
h2
has type
z - 1 ≠ 0
but is expected to have type
?m_2 ≠ 0
state:
z : ℤ,
h : ¬z = 1,
h2 : z - 1 ≠ 0
⊢ (z - 1) / (z - 1) = 1


it looks to me like those types should match?

#### Jalex Stark (Jun 17 2020 at 14:53):

do #check div_self

#### Eric Wieser (Jun 17 2020 at 14:55):

I get div_self : ?M_3 ≠ 0 → ?M_3 / ?M_3 = 1

I don't quite get how it decides to fill the M_3 placeholder. M_3 is implicit, so I was hoping it could be inferred from h2 as z-1.

#### Jalex Stark (Jun 17 2020 at 14:56):

it's going to have a type variable requiring a typeclass that the integers don't satisfy, maybe division_ring or something

#### Eric Wieser (Jun 17 2020 at 14:57):

Is there an equivalent for integers?

#### Reid Barton (Jun 17 2020 at 14:58):

if there is then hopefully it has a name like int.div_self

#### Eric Wieser (Jun 17 2020 at 14:59):

For whatever reason that was not autocompleting...

#### Jalex Stark (Jun 17 2020 at 15:02):

https://leanprover-community.github.io/mathlib_docs/data/int/basic.html#int.div_self

#### Jalex Stark (Jun 17 2020 at 15:02):

do you have import data.int.basic in your file?

#### Kevin Buzzard (Jun 17 2020 at 15:16):

#check @div_self is the thing to do in this situation -- you see immediately what typeclass it wants

Last updated: May 14 2021 at 03:27 UTC