rename Nat.prime_def_lt'' to Nat.prime_def

Stream: mathlib4

[Jon Eugster]

While writing a little tutorial about prime numbers, I noticed particularly one theorem which seems named peculiarly:

theorem Nat.prime_def_lt'' {p : ℕ} : Nat.Prime p ↔ 2 ≤ p ∧ ∀ m, m ∣ p → m = 1 ∨ m = p

It seems to me, this should simply be Nat.prime_def. Especially since there is no "lt" in the statement, and because the docstring of the definition says the following:

/-- `Nat.Prime p` means that `p` is a prime number, that is, a natural number
  at least 2 whose only divisors are `p` and `1`. -/
def Nat.Prime (p : ℕ) :=
  Irreducible p

I've created #19255. Are there good reasons for the current naming or objections against renaming it to Nat.prime_def?

[Mario Carneiro]

sounds reasonable to me (without having looked at all the competitors for that name)

[Daniel Weber]

I agree that this name isn't good, but I feel that _def lemmas should be literally the definition, which is Irreducible p here. I'm not sure about an alternative name, though

[Mario Carneiro]

it's probably best to rename all the prime_def theorems at once, and make sure the naming scheme makes sense across the board

[Mario Carneiro]

(even if the conclusion is that all of them are named correctly except that one)

[Daniel Weber]

@loogle Iff (Nat.Prime _) _

[loogle]

:search: Nat.prime_iff, Nat.prime_def_minFac, and 9 more

[Jon Eugster]

There are a few theorems Nat.prime_def_X, where X is one of minFac, le_sqrt, lt

[Mario Carneiro]

Daniel Weber said:

I agree that this name isn't good, but I feel that _def lemmas should be literally the definition, which is Irreducible p here. I'm not sure about an alternative name, though

I disagree on this. The actual definition should be the one that makes defeq work out nicely, and the thing that is called foo_def is the thing that people are most likely to guess is the definition

[Ruben Van de Velde]

That's probably my fault; anything is fine with me

[Mario Carneiro]

maintaining a strict correspondence with foo and foo_def is missing an opportunity to make mathlib less confusing for people (newcomers and otherwise). Plus, the thing that is literally the definition is already autogenerated as foo.def_eq, we don't need to duplicate that