LucasLehmer.X.card_eq
theorem LucasLehmer.X.card_eq : ∀ {q : ℕ+}, Fintype.card (LucasLehmer.X q) = ↑q ^ 2
This theorem states that the cardinality (or the number of elements) of `X`, as defined in the context of the Lucas-Lehmer sequences, is equal to `q` squared. Here, `X` is a ring constructed as ℤ/qℤ + √3 ℤ/qℤ for a given positive natural number `q`. So for any such `q`, the size of the set `X` (which consists of pairs of integers mod `q`) is `q^2`.
More concisely: The cardinality of the Lucas-Lehmer sequence ring ℤ/qℤ + √3 ℤ/qℤ is equal to q² for any positive natural number q.
|
LucasLehmer.mersenne_coe_X
theorem LucasLehmer.mersenne_coe_X : ∀ (p : ℕ), ↑(mersenne p) = 0
This theorem, named `LucasLehmer.mersenne_coe_X`, stipulates that for any natural number `p`, the Mersenne number of `p`, when cast to another type, equals zero. The Mersenne number of `p` is defined as 2 raised to the power of `p` minus 1. This theorem is related to number theory involving Mersenne numbers, where `q` is identified as the minimum factor of the Mersenne number of `p`, hence the Mersenne number `p` equals zero in the polynomial ring `X q`.
More concisely: For any natural number p, the Mersenne number 2^p - 1 equals zero in the polynomial ring X over the minimum factor q of p.
|
LucasLehmer.X.card_units_lt
theorem LucasLehmer.X.card_units_lt : ∀ {q : ℕ+}, 1 < q → Fintype.card (LucasLehmer.X q)ˣ < ↑q ^ 2
The theorem `LucasLehmer.X.card_units_lt` asserts that for any strictly positive natural number `q` greater than 1, the number of units in the ring `X q`, which is defined as ℤ/qℤ + √3 ℤ/qℤ, is strictly less than `q` squared. This is due to the fact that `0` is not considered as a unit in the ring.
More concisely: The number of units in the ring ℤ/qℤ + √3 ℤ/qℤ, where q > 1, is strictly less than q^2.
|
LucasLehmer.X.ext
theorem LucasLehmer.X.ext : ∀ {q : ℕ+} {x y : LucasLehmer.X q}, x.1 = y.1 → x.2 = y.2 → x = y
The theorem `LucasLehmer.X.ext` states that for any positive natural number `q` and any two elements `x` and `y` of the ring `LucasLehmer.X q` (which is defined as the Cartesian product of ℤ/qℤ and ℤ/qℤ), if the first component of `x` is equal to the first component of `y` and the second component of `x` is equal to the second component of `y`, then `x` is equal to `y`. In other words, two elements of the ring `LucasLehmer.X q` are equal if and only if their corresponding components are equal.
More concisely: In the ring of Lucas-Lehmer quadrates `LucasLehmer.X q`, elements with equal first and second components are equal.
|
LucasLehmer.X.closed_form
theorem LucasLehmer.X.closed_form :
∀ {q : ℕ+} (i : ℕ), ↑(LucasLehmer.s i) = LucasLehmer.X.ω ^ 2 ^ i + LucasLehmer.X.ωb ^ 2 ^ i
This theorem provides a closed form solution for the Lucas-Lehmer sequence, which is a recurrence relation defined such that the (i+1)th term is equal to the square of the ith term minus 2, with the initial term being 4. Specifically, it states that for any positive natural number q and any natural number i, the ith term of the Lucas-Lehmer sequence is equal to the sum of ω (defined as 2 + √3) raised to the power of 2 to the i and ωb (defined as 2 - √3) raised to the power of 2 to the i.
More concisely: The i-th term of the Lucas-Lehmer sequence, defined as the recurrence relation where the (i+1)th term is equal to the square of the ith term minus 2 with initial term 4, equals ω^(2^i) + ω^(-2^i), where ω = 2 + √3.
|
LucasLehmer.two_lt_q
theorem LucasLehmer.two_lt_q : ∀ (p' : ℕ), 2 < LucasLehmer.q (p' + 2)
The theorem `LucasLehmer.two_lt_q` states that for any natural number `p'`, if we increment `p'` by 2 to get `p' + 2` and consider the Mersenne number associated with `p' + 2`, then the smallest prime factor `q` of this Mersenne number (denoted `LucasLehmer.q (p' + 2)`) is always greater than 2.
More concisely: For any natural number `p'`, the smallest prime factor of the Mersenne number `2^(p' + 2) - 1` is greater than 2.
|
LucasLehmer.order_ω
theorem LucasLehmer.order_ω :
∀ (p' : ℕ), lucasLehmerResidue (p' + 2) = 0 → orderOf (LucasLehmer.ωUnit (p' + 2)) = 2 ^ (p' + 2)
The theorem `LucasLehmer.order_ω` states that for any natural number `p'`, if the Lucas-Lehmer residue of `p' + 2` is zero, then the order of the element `ω` in the unit group, denoted by `LucasLehmer.ωUnit (p' + 2)`, is exactly `2^(p' + 2)`. This implies that `ω` is an element of the group with order `2^(p' + 2)` under the condition that the Lucas-Lehmer residue equals zero. The order of an element in a group is the smallest positive integer `n` such that the element raised to `n` power equals the identity of the group. In this case, if `x` is `ω` and the group is the unit group, then `x^n` or `ω^(2^(p' + 2))` would be the identity element in the group.
More concisely: If the Lucas-Lehmer residue of a natural number `p'` is zero, then the order of `ω` in the unit group of `\mathbb{Z}/(p' + 2)\mathbb{Z}` is `2^(p' + 2)`.
|