prime_or_zero for naturals

Stream: Is there code for X?

[Chris Hughes]

I have a field of characteristic p where p is either a prime or zero. I need the fact that zmod p is an integral domain. Is there an easy way of doing this?

[Alex J. Best]

I don't know what a nice way to express prime or zero for naturals is, you could say that the ideal generated in Z is prime but thats a bit OTT.
Does this work for you:

import data.zmod.basic

variables (p : ℕ)
instance [fact (nat.prime p)] : euclidean_domain (zmod p) :=
field.to_euclidean_domain --not really needed tbh
instance zmod_zero.euclidean_domain : euclidean_domain (zmod 0) :=
int.euclidean_domain

def bleh (h : p = 0 ∨ p.prime) : euclidean_domain (zmod p) := begin
  by_cases hp : p = 0,
  { rw hp,
    apply_instance, },
  { haveI : fact (p.prime) := fact.mk (h.resolve_left hp),
    apply_instance, }
end

[Chris Hughes]

The problem is bleh isn't an instance. I guess you need h to be wrapped in fact

[Alex J. Best]

Yeah exactly, seeing as the condition =0 or prime isn't as common as just prime it seems unlikely you'll ever have tc search find it automatically anyway

[Yaël Dillies]

I also guess you will want two distinct instances anyway.

[Alex J. Best]

You could make instance {K : Type*} [field K] {p : ℕ} [char_p K p] : integral_domain (zmod p) but that seems like a dangerous instance, but maybe you can make it a local instance for your context?

[Adam Topaz]

This is a job for docs#exp_char

[Chris Hughes]

I think that exp_char file needs more documentation. I don't really understand what it's for.

[Eric Wieser]

ping @Jakob Scholbach who added it

[Jakob Scholbach]

@Chris Hughes what exactly do you think needs more documentation?