WithBot v WithZero

Stream: mathlib4

[Kevin Buzzard]

I'm in the middle of a bunch of rewrites and I don't really want to stop, apply norm_cast, and then start again. But I can't find a way around it:

import Mathlib.RingTheory.DedekindDomain.AdicValuation

example (x : Multiplicative ℤ) (hx : 1 < (x : WithZero (Multiplicative ℤ))) : 1 < x := by
  rw [WithBot.one_lt_coe] at hx -- fails

because we have WithBot.one_lt_coe but it won't fire on WithZero. Not even this works:

example (x : Multiplicative ℤ) (hx : 1 < (x : WithZero (Multiplicative ℤ))) : 1 < x := by
  rw [(WithBot.one_lt_coe : (1 : WithZero (Multiplicative ℤ)) < ↑x ↔ _)] at hx -- fails

Should I just make WithZero.one_lt_coe or is this frowned upon because it's code duplication?

[Yaël Dillies]

It's not code duplication! They are (supposed to be) different types!

[Kevin Buzzard]

#13853