From 96eb16d55cbe6ff905346761994d815d46151112 Mon Sep 17 00:00:00 2001 From: yuanyi-350 Date: Thu, 23 Apr 2026 16:30:55 +0800 Subject: [PATCH] refactor(NumberTheory): golf GaussEisensteinLemmas --- .../LegendreSymbol/GaussEisensteinLemmas.lean | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean b/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean index 44961ac970d49b..b6bd0e447a5270 100644 --- a/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean +++ b/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean @@ -74,14 +74,8 @@ private theorem gauss_lemma_aux₁ (p : ℕ) [Fact p.Prime] {a : ℤ} (hap : (a split_ifs <;> simp) _ = (-1 : ZMod p) ^ #{x ∈ Ico 1 (p / 2).succ | ¬(a * x.cast : ZMod p).val ≤ p / 2} * ∏ x ∈ Ico 1 (p / 2).succ, ↑((a * x : ZMod p).valMinAbs.natAbs) := by - have : - (∏ x ∈ Ico 1 (p / 2).succ, if (a * x : ZMod p).val ≤ p / 2 then (1 : ZMod p) else -1) = - ∏ x ∈ Ico 1 (p / 2).succ with ¬(a * x.cast : ZMod p).val ≤ p / 2, -1 := - prod_bij_ne_one (fun x _ _ => x) - (fun x => by split_ifs <;> (dsimp; simp_all)) - (fun _ _ _ _ _ _ => id) (fun b h _ => ⟨b, by simp_all [-not_le]⟩) - (by intros; split_ifs at * <;> simp_all) - rw [prod_mul_distrib, this, prod_const] + rw [prod_mul_distrib, Finset.prod_ite] + simp _ = (-1 : ZMod p) ^ #{x ∈ Ico 1 (p / 2).succ | ¬(a * x.cast : ZMod p).val ≤ p / 2} * (p / 2)! := by rw [← prod_natCast, Finset.prod_eq_multiset_prod,