From 61f3a115798b5f6da0b5f3d1f5e7d19271a81ce7 Mon Sep 17 00:00:00 2001 From: Alex J Best Date: Fri, 29 Dec 2023 14:23:37 +0000 Subject: [PATCH 1/2] chore: mark neg_div_neg_eq as simp --- Mathlib/Algebra/Field/Basic.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/Algebra/Field/Basic.lean b/Mathlib/Algebra/Field/Basic.lean index 720e6cc73e8ce..94a8f28485fd1 100644 --- a/Mathlib/Algebra/Field/Basic.lean +++ b/Mathlib/Algebra/Field/Basic.lean @@ -118,6 +118,7 @@ theorem neg_div (a b : K) : -b / a = -(b / a) := by theorem neg_div' (a b : K) : -(b / a) = -b / a := by simp [neg_div] #align neg_div' neg_div' +@[simp] theorem neg_div_neg_eq (a b : K) : -a / -b = a / b := by rw [div_neg_eq_neg_div, neg_div, neg_neg] #align neg_div_neg_eq neg_div_neg_eq From 58bd95d1892fab3b340b34c24911053afe5f20c8 Mon Sep 17 00:00:00 2001 From: Alex J Best Date: Fri, 29 Dec 2023 15:34:34 +0000 Subject: [PATCH 2/2] fix nontermin --- Mathlib/NumberTheory/ModularForms/JacobiTheta/Basic.lean | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/Mathlib/NumberTheory/ModularForms/JacobiTheta/Basic.lean b/Mathlib/NumberTheory/ModularForms/JacobiTheta/Basic.lean index dd26ade756470..2c842c7b6a039 100644 --- a/Mathlib/NumberTheory/ModularForms/JacobiTheta/Basic.lean +++ b/Mathlib/NumberTheory/ModularForms/JacobiTheta/Basic.lean @@ -100,9 +100,11 @@ theorem jacobiTheta_S_smul (τ : ℍ) : rw [mul_comm ((1 : ℂ) / _) _, mul_one_div, eq_div_iff ha', mul_comm _ (_ ^ _), eq_comm] at this have expo1 : ∀ n : ℤ, -↑π / (-I * ↑τ) * (n : ℂ) ^ 2 = ↑π * I * (n : ℂ) ^ 2 * (-↑τ)⁻¹ := by intro n - field_simp [hτ, I_ne_zero] + simp only [neg_mul, neg_div_neg_eq, div_mul_eq_mul_div, inv_eq_one_div, mul_div_assoc', mul_one, + ne_eq, neg_eq_zero, hτ, not_false_eq_true, eq_div_iff, I_ne_zero, + mul_ne_zero, div_eq_iff] ring_nf - rw [I_sq, mul_neg, mul_one, neg_neg] + rw [I_sq, mul_neg, mul_one] simp_rw [expo1] at this have expo2 : ∀ n : ℤ, -↑π * (-I * ↑τ) * (n : ℂ) ^ 2 = ↑π * I * (n : ℂ) ^ 2 * ↑τ := by intro n