prime in `ring_theory/associated.lean`

Stream: general

[Scott Morrison]

ring_theory/associated.lean defines

/-- prime element of a semiring -/
def prime [comm_semiring α] (p : α) : Prop :=
p ≠ 0 ∧ ¬ is_unit p ∧ (∀a b, p ∣ a * b → p ∣ a ∨ p ∣ b)

in the root namespace, which then causes clashes with nat.prime if you have nat open.

[Scott Morrison]

Could we rename or namespace this? @Johannes Hölzl introduced it here.

[Chris Hughes]

We could just get rid of nat prime as well.

[Kenny Lau]

wat @_@

[Scott Morrison]

What do you mean, @Chris Hughes?

[Chris Hughes]

Just get rid of nat.prime and use prime in its place. I just realized that currently nat.prime is basically irreducible , so this would be a non trivial redactor.

[Scott Morrison]

Oh, I see! That sounds both a good idea and ambitious. :-)

[Scott Morrison]

Is there a good fix in the meantime?

[Johan Commelin]

I would just call this one ring.prime

[Mario Carneiro]

I'm okay with ring.prime if the kill nat.prime thing doesn't work

[Mario Carneiro]

although I've already fixed some bugs caused by this in the library (adding nat.prime when nat was open), maybe they should be re-ambiguated if it lands?