induction principle for `ℤₘ₀`

Stream: Is there code for X?

[Kevin Buzzard]

ℤₘ₀ is mathlib's notation for WithZero (Multiplicative Int):

scoped[DiscreteValuation] notation "ℤₘ₀" => WithZero (Multiplicative ℤ)

Having been supervising a student who is using it, I'm struggling to find things like a decent induction principle for it. Do we have something like this:

import Mathlib.RingTheory.Valuation.Basic

open scoped DiscreteValuation -- for ℤₘ₀ notation

open Multiplicative -- so I can type `ofAdd` instead of `Multiplicative.ofAdd`

@[elab_as_elim]
protected def Zm0.induction_on {motive : ℤₘ₀ → Prop} (zero : motive 0)
  (of_int : ∀ z : ℤ, motive (ofAdd z : Multiplicative ℤ)) (x : ℤₘ₀) : motive x :=
WithZero.recZeroCoe zero of_int x

? If not, do we want it or is there some trick I'm missing whereby we can avoid this boilerplate? Furthermore, what to do about the namespace? Is it OK to make a new namespace Zmo for basic results about this type? It's a fundamental object in Lean's set-up of the theory of discrete valuations.

[Eric Wieser]

#14729 will help here

[Eric Wieser]

With that, you can at least write cases' x with x <;> [skip, cases x] or

cases x with
| zero => sorry
| coe x =>
  cases x with | _ x => ?_
  sorry

or similar