Merge branch 'master' into zfset_omega

Author: staroperator

.github/build.in.yml

@@ -522,7 +522,7 @@ jobs:
             if timeout 15m env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee ".lake/lint_output_attempt_${attempt}.txt"; then
               break
             fi
-            status=$?
+            status=${PIPESTATUS[0]}
             if grep -q "cannot parse arguments" ".lake/lint_output_attempt_${attempt}.txt"; then
               echo ""
               echo "=============================================================================="

.github/workflows/bors.yml

@@ -532,7 +532,7 @@ jobs:
             if timeout 15m env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee ".lake/lint_output_attempt_${attempt}.txt"; then
               break
             fi
-            status=$?
+            status=${PIPESTATUS[0]}
             if grep -q "cannot parse arguments" ".lake/lint_output_attempt_${attempt}.txt"; then
               echo ""
               echo "=============================================================================="

.github/workflows/build.yml

@@ -538,7 +538,7 @@ jobs:
             if timeout 15m env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee ".lake/lint_output_attempt_${attempt}.txt"; then
               break
             fi
-            status=$?
+            status=${PIPESTATUS[0]}
             if grep -q "cannot parse arguments" ".lake/lint_output_attempt_${attempt}.txt"; then
               echo ""
               echo "=============================================================================="

.github/workflows/build_fork.yml

@@ -536,7 +536,7 @@ jobs:
             if timeout 15m env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee ".lake/lint_output_attempt_${attempt}.txt"; then
               break
             fi
-            status=$?
+            status=${PIPESTATUS[0]}
             if grep -q "cannot parse arguments" ".lake/lint_output_attempt_${attempt}.txt"; then
               echo ""
               echo "=============================================================================="

Counterexamples.lean

@@ -11,6 +11,7 @@ import Counterexamples.GameMultiplication
 import Counterexamples.Girard
 import Counterexamples.HeawoodUnitDistance
 import Counterexamples.HomogeneousPrimeNotPrime
+import Counterexamples.InvertibleModuleNotIdeal
 import Counterexamples.IrrationalPowerOfIrrational
 import Counterexamples.MapFloor
 import Counterexamples.MonicNonRegular

Counterexamples/InvertibleModuleNotIdeal.lean

@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2025 Junyan Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Junyan Xu
+-/
+import Mathlib.Algebra.TrivSqZeroExt
+import Mathlib.Data.DFinsupp.Module
+import Mathlib.RingTheory.PicardGroup
+
+/-!
+# A class of examples of invertible modules that are not isomorphic to ideals
+
+References: https://math.stackexchange.com/a/5090562 or https://mathoverflow.net/a/499258
+-/
+
+variable (R : Type*) [CommRing R]
+
+/-- The trivial square-zero extension of a commutative ring R given by the direct sum
+R ⊕ ⨁ₘ R⧸m where m ranges over maximal ideals of R. -/
+abbrev SqZeroExtQuotMax := TrivSqZeroExt R (Π₀ m : MaximalSpectrum R, R ⧸ m.1)
+
+instance : IsFractionRing (SqZeroExtQuotMax R) (SqZeroExtQuotMax R) :=
+  IsFractionRing.self_iff_nonZeroDivisors_le_isUnit.mpr fun x hx ↦
+    TrivSqZeroExt.isUnit_iff_isUnit_fst.mpr <| of_not_not fun hr ↦ by
+    have ⟨M, hM, hrM⟩ := exists_max_ideal_of_mem_nonunits hr
+    classical
+    have := hx.1 (.inr <| .single ⟨M, hM⟩ 1) <| by
+      ext1; · simp
+      simpa [-DFinsupp.single_apply, ← DFinsupp.single_smul, DFinsupp.single_eq_zero]
+        using (Ideal.Quotient.mk_eq_mk_iff_sub_mem ..).mpr (by simpa)
+    simpa using congr(($this).snd)
+
+/-- R as an algebra over `SqZeroExtQuotMax R`. -/
+abbrev SqZeroExtQuotMax.algebraBase : Algebra (SqZeroExtQuotMax R) R := TrivSqZeroExt.algebraBase ..
+
+open CommRing (Pic) in
+/-- If the Picard group of a commutative ring R is nontrivial, then `SqZeroExtQuotMax R`
+has an invertible module (which is the base change of an invertible ideal of R)
+not isomorphic to any ideal. -/
+theorem SqZeroExtQuotMax.not_exists_linearEquiv_ideal_of_invertible [Nontrivial (Pic R)] :
+    ∃ M : Pic (SqZeroExtQuotMax R),
+    ¬ ∃ I : Ideal (SqZeroExtQuotMax R), Nonempty (M ≃ₗ[SqZeroExtQuotMax R] I) := by
+  by_contra! h
+  have ⟨M, hM⟩ := exists_ne (1 : Pic R)
+  have ⟨I, ⟨eI⟩⟩ := h (M.mapAlgebra R _)
+  have ⟨J, ⟨eJ⟩⟩ := h (M⁻¹.mapAlgebra R _)
+  have := Module.Invertible.congr eI
+  have := Module.Invertible.congr eJ
+  obtain ⟨rfl | rfl⟩ := I.eq_top_of_mk_tensor_eq_one J <| by
+    rw [Pic.mk_tensor, ← Pic.mk_eq_mk_iff.mpr ⟨eI⟩, ← Pic.mk_eq_mk_iff.mpr ⟨eJ⟩,
+      Pic.mk_eq_self, Pic.mk_eq_self, ← map_mul, mul_inv_cancel, map_one]
+  have eq := Pic.mk_eq_one_iff.mpr ⟨eI ≪≫ₗ Submodule.topEquiv⟩
+  rw [Pic.mk_eq_self] at eq
+  let := TrivSqZeroExt.algebraBase
+  have eq := congr(Pic.mapAlgebra (SqZeroExtQuotMax R) R $eq)
+  exact hM <| by rwa [map_one, Pic.mapAlgebra_mapAlgebra, Pic.mapAlgebra_self] at eq

Mathlib.lean

@@ -1569,6 +1569,7 @@ public import Mathlib.Analysis.Calculus.ContDiff.Polynomial
 public import Mathlib.Analysis.Calculus.ContDiff.RCLike
 public import Mathlib.Analysis.Calculus.ContDiff.RestrictScalars
 public import Mathlib.Analysis.Calculus.ContDiff.WithLp
+public import Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
 public import Mathlib.Analysis.Calculus.DSlope
 public import Mathlib.Analysis.Calculus.Darboux
 public import Mathlib.Analysis.Calculus.Deriv.Abs

Mathlib/Algebra/Algebra/Basic.lean

@@ -431,8 +431,8 @@ instance (priority := 120) IsScalarTower.to_smulCommClass : SMulCommClass R A M
 instance (priority := 110) IsScalarTower.to_smulCommClass' : SMulCommClass A R M :=
   SMulCommClass.symm _ _ _
 
--- see Note [lower instance priority]
-instance (priority := 200) Algebra.to_smulCommClass {R A} [CommSemiring R] [Semiring A]
+/-- This has high priority because it is almost always the right instance when it applies. -/
+instance (priority := high) Algebra.to_smulCommClass {R A} [CommSemiring R] [Semiring A]
     [Algebra R A] : SMulCommClass R A A :=
   IsScalarTower.to_smulCommClass
 

Mathlib/Algebra/BigOperators/Finprod.lean

@@ -545,6 +545,8 @@ theorem one_lt_finprod_cond {M : Type*} [CommMonoid M] [PartialOrder M] [IsOrder
     · aesop
   · simp +contextual
 
+@[deprecated (since := "2026-01-06")] alias finprod_cond_pos := finsum_cond_pos
+
 @[to_additive finsum_pos]
 theorem one_lt_finprod {M : Type*} [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M]
     {f : ι → M}

Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

@@ -347,15 +347,15 @@ theorem prod_eq_single {s : Finset ι} {f : ι → M} (a : ι) (h₀ : ∀ b ∈
 @[to_additive (attr := simp)]
 lemma prod_ite_mem_eq [Fintype ι] (s : Finset ι) (f : ι → M) [DecidablePred (· ∈ s)] :
     (∏ i, if i ∈ s then f i else 1) = ∏ i ∈ s, f i := by
-  rw [← Finset.prod_filter]; congr; aesop
+  rw [← Finset.prod_filter]; congr; grind
 
 @[to_additive]
 lemma prod_eq_ite [DecidableEq ι] {s : Finset ι} {f : ι → M} (a : ι)
     (h₀ : ∀ b ∈ s, b ≠ a → f b = 1) :
     ∏ x ∈ s, f x = if a ∈ s then f a else 1 := by
   by_cases h : a ∈ s
   · simp [Finset.prod_eq_single_of_mem a h h₀, h]
-  · replace h₀ : ∀ b ∈ s, f b = 1 := by aesop
+  · replace h₀ : ∀ b ∈ s, f b = 1 := by grind
     simp +contextual [h₀]
 
 @[to_additive]