What is a good name for theorems in mathlib?

Stream: mathlib4

[Stepan Holub]

Hello,
I have an open PR with the following theorem:

theorem name1 (w : List α) (p q : ℕ) (per_p : HasPeriod w p) (per_q : HasPeriod w q)
    (len : p + q - p.gcd q ≤ w.length) : HasPeriod w (p.gcd q)

It is known as the Periodicity Lemma, or as the Fine and Wilf Theorem.

I also plan to submit its generalization for more periods:

 theorem name2 (P : Finset ℕ) (w : List ℕ) (len: fwlength P < w.length) (periods: ∀ p ∈ P\{0}, HasPeriod w p) : HasPeriod w (P.gcd id)

I wanted to call the name1 periodicity_lemma, and the name2 multiperiodicity_lemma. But
@Martin Dvořák suggested name1 to be hasPeriod_gcd.

What is more suitable for mathlib? And what should be name2 then?

[Robin Arnez]

The convention is usually to name theorems structurally so you find them more easily.
name1 should probably even be HasPeriod.gcd so you can use hp.gcd hq hlen here.
name2 could be named hasPeriod_finsetGcd or hasPeriod_gcd_of_fwlength_lt (or, really, any contraction of hasPeriod_finsetGcd_id_of_fwlength_lt_length_of_forall_mem_sdiff_singleton_zero_hasPeriod)

[Alfredo Moreira-Rosa]

maybe, Finset.HasPeriod.gcd would also work for name2 ?

[Aaron Liu]

I suggested HasPeriod.finsetGcd

[Stepan Holub]

Aaron Liu said:

I suggested HasPeriod.finsetGcd

How would that work? There is no HasPeriod in assumptions, so I see no possible h.finsetGcd. Perhaps something like HasAllPeriods.finsetGcd with

def HasAllPeriods (P : Finset ℕ) (w : List α) := ∀ x ∈ P, HasPeriod w x

[Jakub Nowak]

So maybe hasPeriod_finsetGcd? Though, even if it cannot be used with dot syntax it can still be named HasPeriod.finsetGcd just because of analogy with HasPeriod.gcd.

[Robin Arnez]

I guess you could still use .finsetGcd ... though

[Stepan Holub]

Robin Arnez said:

I guess you could still use .finsetGcd ... though

Can you explain how?

[Robin Arnez]

Well there are two kinds of dot notation:

#check (3).succ
#check (.succ 3 : Nat)

The first one works based on the type of the inner expression and the second one works based on the expected type. So if you had the expected type HasPeriod x (P.gcd id), you could use .finsetGcd to refer to HasPeriod.finsetGcd

[Stepan Holub]

I see, like in

example (P : Finset ℕ) (w : List ℕ) : HasPeriod w (P.gcd id) := by
   refine .finsetGcd ?_ ?_ ?_ ?_
   ...

Although I do not see much of an advantage here.