Formalize the infinitude conjecture for decimal repunit primes

### What is the conjecture

A decimal repunit is a natural number consisting only of the digit `1`. The repunit of length
$n\geq1$ is

$$
R_n=1+10+10^2+\cdots+10^{n-1}=\frac{10^n-1}{9}.
$$

For example, $R_2=11$ is prime, while $R_3=111=3\cdot37$ is composite. The next known prime
examples occur at lengths $19$ and $23$.

Wikipedia states:

> It has been conjectured that there are infinitely many repunit primes.

References:

- [Wikipedia: Repunit](https://en.wikipedia.org/wiki/Repunit#Decimal_repunit_primes)
- [OEIS A002275](https://oeis.org/A002275), decimal repunits
- [OEIS A004022](https://oeis.org/A004022), decimal repunit primes
- [OEIS A004023](https://oeis.org/A004023), lengths of decimal repunit primes

The formalization defines $R_n$ as a finite geometric sum and states that infinitely many lengths
produce a prime.

### Prerequisites needed

Mathlib already provides finite sums, natural-number exponentiation, primality, and `Set.Infinite`.
Using the geometric sum avoids natural-number division in the definition. No addition to
`FormalConjecturesForMathlib` is needed.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

- ams-11

### Choose either option

- [x] I plan on adding this conjecture to the repository
- [ ] This issue is up for grabs: I would like to see this conjecture added by somebody else

Start by locating existing conjecture formalizations in the repository and reviewing mathlib's finite sums, natural-number exponentiation, primality, and Set.Infinite APIs. Define the decimal repunit as the stated finite geometric sum and formalize that infinitely many lengths produce a prime; it is done when the theorem compiles.

Written by the indexing model from the issue text.