ZMod 0

Stream: mathlib4

[Michael Stoll]

Are there objections to adding

instance : CanLift (ZMod 0) ℤ (↑) (fun _ ↦ True) where
  prf x _ := ⟨x.valMinAbs, rfl⟩

lemma ZMod.isUnit_zMod_zero_iff (m : ZMod 0) : IsUnit m ↔ m = 1 ∨ m = -1 := by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · lift m to ℤ using trivial
    obtain ⟨x, hx⟩ := isUnit_iff_exists_inv.mp h
    lift x to ℤ using trivial
    exact_mod_cast Int.isUnit_iff.mp <| isUnit_iff_exists_inv.mpr ⟨x, hx⟩
  · rcases h with rfl | rfl
    · exact isUnit_one
    · exact isUnit_neg_one

to Data.ZMod.Basic? (Golf welcome) @Floris van Doorn (who seems to have written the lift tactic originally)

[Ruben Van de Velde]

Using lift for this seems quite surprising

[Michael Stoll]

How would you do it?

[Michael Stoll]

If we had a ring isomorphism with the integers, one could transport stuff, I assume.

[Ruben Van de Velde]

lemma ZMod.isUnit_zMod_zero_iff (m : ZMod 0) : IsUnit m ↔ m = 1 ∨ m = -1 :=
  Int.isUnit_iff

[Michael Stoll]

This is way too simple :smile:
Is this defeq abuse?

[Ruben Van de Velde]

It's defeq use. Up to you whether it's abuse :)

[Michael Stoll]

But thanks for pointing this out!

[Yaël Dillies]

I am pretty sure docs#ZMod is defined the way it is precisely so that one may look through the definition.

[Ruben Van de Velde]

I guess the other question is why you're using ZMod 0

[Michael Stoll]

The reason I need this is that I want to prove something for ZMod n without assumptions on n.

[Yaël Dillies]

Yeah then look through as much as you want.