From 35c984e27ebc56768a62750eca34b03821fe70d5 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 30 Apr 2024 04:24:41 +0000 Subject: [PATCH] chore: HahnSeries.ofPowerSeries_X_pow linter complains on nightly-testing (#12529) On `nightly-testing` `ofPowerSeries_X_pow` becomes a bad simp lemma, because the LHS will simplify. Fix this by adding the missing lemma so the whole proof is just by `simp`, and remove `@[simp]`. Co-authored-by: Scott Morrison --- Mathlib/RingTheory/HahnSeries/Multiplication.lean | 12 ++++++++++++ Mathlib/RingTheory/HahnSeries/PowerSeries.lean | 10 ++-------- 2 files changed, 14 insertions(+), 8 deletions(-) diff --git a/Mathlib/RingTheory/HahnSeries/Multiplication.lean b/Mathlib/RingTheory/HahnSeries/Multiplication.lean index 8ba32e53907f8..9c1c0701e0774 100644 --- a/Mathlib/RingTheory/HahnSeries/Multiplication.lean +++ b/Mathlib/RingTheory/HahnSeries/Multiplication.lean @@ -442,6 +442,18 @@ theorem single_mul_single {a b : Γ} {r s : R} : end NonUnitalNonAssocSemiring +section Semiring + +variable [Semiring R] + +@[simp] +theorem single_pow (a : Γ) (n : ℕ) (r : R) : single a r ^ n = single (n • a) (r ^ n) := by + induction' n with n IH + · simp; rfl + · rw [pow_succ, pow_succ, IH, single_mul_single, succ_nsmul] + +end Semiring + section NonAssocSemiring variable [NonAssocSemiring R] diff --git a/Mathlib/RingTheory/HahnSeries/PowerSeries.lean b/Mathlib/RingTheory/HahnSeries/PowerSeries.lean index c9eb3b9ff110d..7333c59babf9f 100644 --- a/Mathlib/RingTheory/HahnSeries/PowerSeries.lean +++ b/Mathlib/RingTheory/HahnSeries/PowerSeries.lean @@ -142,15 +142,9 @@ theorem ofPowerSeries_X : ofPowerSeries Γ R PowerSeries.X = single 1 1 := by simp (config := { contextual := true }) [Ne.symm hn] #align hahn_series.of_power_series_X HahnSeries.ofPowerSeries_X -@[simp] -theorem ofPowerSeries_X_pow {R} [CommSemiring R] (n : ℕ) : +theorem ofPowerSeries_X_pow {R} [Semiring R] (n : ℕ) : ofPowerSeries Γ R (PowerSeries.X ^ n) = single (n : Γ) 1 := by - rw [RingHom.map_pow] - induction' n with n ih - · simp - rfl - · rw [pow_succ, ih, ofPowerSeries_X, mul_comm, single_mul_single, one_mul, - Nat.cast_succ, add_comm] + simp #align hahn_series.of_power_series_X_pow HahnSeries.ofPowerSeries_X_pow -- Lemmas about converting hahn_series over fintype to and from mv_power_series