Natural number division partial function

Stream: new members

[Jesse Slater]

I want to do division of natural numbers as a partial function where only division with no remainder is allowed.
I can do it with this function:

def optional_division (n m : Nat) : Option Nat :=
  if n % m = 0
  then Option.some (n / m)
  else Option.none

Is there some built in function for this?
What would be a good way to search for built in functions?

[Martin Dvořák]

I don't think we have it. We avoid partial functions.

[Martin Dvořák]

@loogle (Nat -> Nat -> Option Nat)

[Martin Dvořák]

@loogle (Nat -> Nat -> Option Nat)

[loogle]

:search: Array.findIdx?.loop, Lean.Compiler.LCNF.Simp.isJpCases?.go, and 4 more

[Martin Dvořák]

To my surprise, we have this weird subtraction:
https://github.com/leanprover-community/mathlib4/blob/51089d8f290c06725d47f07f60d0e42d83f6474b/Mathlib/Data/Nat/PSub.lean#L117-L118

[Jesse Slater]

loogle seems like the best answer to this question.
Being able to look up type signatures will be very helpful, thank you!

[Kevin Buzzard]

I think you've defined 0/0 to be 0, just checking you're ok with that