From 83d958a874401834b9372344178a03874b4b4eb6 Mon Sep 17 00:00:00 2001 From: yuanyi-350 Date: Sat, 25 Apr 2026 09:59:17 +0800 Subject: [PATCH 1/3] refactor(NumberTheory): golf PellMatiyasevic --- Mathlib/NumberTheory/PellMatiyasevic.lean | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/Mathlib/NumberTheory/PellMatiyasevic.lean b/Mathlib/NumberTheory/PellMatiyasevic.lean index 6d37f7176a03e6..49a8a2878b03d3 100644 --- a/Mathlib/NumberTheory/PellMatiyasevic.lean +++ b/Mathlib/NumberTheory/PellMatiyasevic.lean @@ -469,13 +469,7 @@ theorem dvd_of_ysq_dvd {n t} (h : yn a1 n * yn a1 n ∣ yn a1 t) : yn a1 n ∣ t set_option backward.isDefEq.respectTransparency false in theorem pellZd_succ_succ (n) : pellZd a1 (n + 2) + pellZd a1 n = (2 * a : ℕ) * pellZd a1 (n + 1) := by - have : (1 : ℤ√(d a1)) + ⟨a, 1⟩ * ⟨a, 1⟩ = ⟨a, 1⟩ * (2 * a) := by - rw [Zsqrtd.natCast_val] - change (⟨_, _⟩ : ℤ√(d a1)) = ⟨_, _⟩ - rw [dz_val] - dsimp [az] - ext <;> dsimp <;> ring_nf - simpa [mul_add, mul_comm, mul_left_comm, add_comm] using congr_arg (· * pellZd a1 n) this + ext <;> simp [pellZd, xn_succ, yn_succ, dz_val, az] <;> ring_nf theorem xy_succ_succ (n) : xn a1 (n + 2) + xn a1 n = From 1c154ec9da2d7818d28caf60eda642d0049dcb81 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Sat, 25 Apr 2026 10:03:23 +0800 Subject: [PATCH 2/3] Update PellMatiyasevic.lean --- Mathlib/NumberTheory/PellMatiyasevic.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/NumberTheory/PellMatiyasevic.lean b/Mathlib/NumberTheory/PellMatiyasevic.lean index 49a8a2878b03d3..1c73b63955062a 100644 --- a/Mathlib/NumberTheory/PellMatiyasevic.lean +++ b/Mathlib/NumberTheory/PellMatiyasevic.lean @@ -466,7 +466,6 @@ theorem dvd_of_ysq_dvd {n t} (h : yn a1 n * yn a1 n ∣ yn a1 t) : yn a1 n ∣ t rw [ke] exact dvd_mul_of_dvd_right (((xy_coprime _ _).pow_left _).symm.dvd_of_dvd_mul_right this) _ -set_option backward.isDefEq.respectTransparency false in theorem pellZd_succ_succ (n) : pellZd a1 (n + 2) + pellZd a1 n = (2 * a : ℕ) * pellZd a1 (n + 1) := by ext <;> simp [pellZd, xn_succ, yn_succ, dz_val, az] <;> ring_nf From 9ee2889319701ad397a466e6b395d9abade5c5f4 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Mon, 27 Apr 2026 08:35:18 +0800 Subject: [PATCH 3/3] Update Mathlib/NumberTheory/PellMatiyasevic.lean Co-authored-by: David Loeffler --- Mathlib/NumberTheory/PellMatiyasevic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/NumberTheory/PellMatiyasevic.lean b/Mathlib/NumberTheory/PellMatiyasevic.lean index 1c73b63955062a..dbec7222757b75 100644 --- a/Mathlib/NumberTheory/PellMatiyasevic.lean +++ b/Mathlib/NumberTheory/PellMatiyasevic.lean @@ -468,7 +468,7 @@ theorem dvd_of_ysq_dvd {n t} (h : yn a1 n * yn a1 n ∣ yn a1 t) : yn a1 n ∣ t theorem pellZd_succ_succ (n) : pellZd a1 (n + 2) + pellZd a1 n = (2 * a : ℕ) * pellZd a1 (n + 1) := by - ext <;> simp [pellZd, xn_succ, yn_succ, dz_val, az] <;> ring_nf + ext <;> simp [dz_val, az] <;> ring_nf theorem xy_succ_succ (n) : xn a1 (n + 2) + xn a1 n =