Using div_self

Stream: new members

[Eric Wieser]

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]

do #check div_self

[Eric Wieser]

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]

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

[Eric Wieser]

Is there an equivalent for integers?

[Reid Barton]

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

[Eric Wieser]

For whatever reason that was not autocompleting...

[Jalex Stark]

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

[Jalex Stark]

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

[Kevin Buzzard]

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