Trigger CI for leanprover-community/batteries#1267

Author: leanprover-community-mathlib4-bot

.github/build.in.yml

@@ -422,6 +422,7 @@ jobs:
 
   post_steps:
     name: Post-Build StepJOB_NAME
+    if: FORK_CONDITION
     needs: [build]
     runs-on: ubuntu-latest # Note these steps run on disposable GitHub runners, so no landrun sandboxing is needed.
     steps:
@@ -503,13 +504,24 @@ jobs:
 
   style_lint:
     name: Lint styleJOB_NAME
+    if: FORK_CONDITION
     runs-on: ubuntu-latest
     steps:
       - uses: leanprover-community/lint-style-action@f2e7272aad56233a642b08fe974cf09dd664b0c8 # 2025-05-22
         with:
           mode: check
           lint-bib-file: true
 
+  build_and_lint:
+    name: CI Success
+    if: FORK_CONDITION
+    needs: [style_lint, build]
+    runs-on: ubuntu-latest
+    steps:
+      - name: succeed
+        run: |
+          echo "Success: Required build and lint checks completed!"
+
   final:
     name: Post-CI jobJOB_NAME
     if: FORK_CONDITION

.github/workflows/bors.yml

@@ -432,6 +432,7 @@ jobs:
 
   post_steps:
     name: Post-Build Step
+    if: true
     needs: [build]
     runs-on: ubuntu-latest # Note these steps run on disposable GitHub runners, so no landrun sandboxing is needed.
     steps:
@@ -513,13 +514,24 @@ jobs:
 
   style_lint:
     name: Lint style
+    if: true
     runs-on: ubuntu-latest
     steps:
       - uses: leanprover-community/lint-style-action@f2e7272aad56233a642b08fe974cf09dd664b0c8 # 2025-05-22
         with:
           mode: check
           lint-bib-file: true
 
+  build_and_lint:
+    name: CI Success
+    if: true
+    needs: [style_lint, build]
+    runs-on: ubuntu-latest
+    steps:
+      - name: succeed
+        run: |
+          echo "Success: Required build and lint checks completed!"
+
   final:
     name: Post-CI job
     if: true

.github/workflows/build.yml

@@ -439,6 +439,7 @@ jobs:
 
   post_steps:
     name: Post-Build Step
+    if: true
     needs: [build]
     runs-on: ubuntu-latest # Note these steps run on disposable GitHub runners, so no landrun sandboxing is needed.
     steps:
@@ -520,13 +521,24 @@ jobs:
 
   style_lint:
     name: Lint style
+    if: true
     runs-on: ubuntu-latest
     steps:
       - uses: leanprover-community/lint-style-action@f2e7272aad56233a642b08fe974cf09dd664b0c8 # 2025-05-22
         with:
           mode: check
           lint-bib-file: true
 
+  build_and_lint:
+    name: CI Success
+    if: true
+    needs: [style_lint, build]
+    runs-on: ubuntu-latest
+    steps:
+      - name: succeed
+        run: |
+          echo "Success: Required build and lint checks completed!"
+
   final:
     name: Post-CI job
     if: true

.github/workflows/build_fork.yml

@@ -436,6 +436,7 @@ jobs:
 
   post_steps:
     name: Post-Build Step (fork)
+    if: github.event.pull_request.head.repo.fork
     needs: [build]
     runs-on: ubuntu-latest # Note these steps run on disposable GitHub runners, so no landrun sandboxing is needed.
     steps:
@@ -517,13 +518,24 @@ jobs:
 
   style_lint:
     name: Lint style (fork)
+    if: github.event.pull_request.head.repo.fork
     runs-on: ubuntu-latest
     steps:
       - uses: leanprover-community/lint-style-action@f2e7272aad56233a642b08fe974cf09dd664b0c8 # 2025-05-22
         with:
           mode: check
           lint-bib-file: true
 
+  build_and_lint:
+    name: CI Success
+    if: github.event.pull_request.head.repo.fork
+    needs: [style_lint, build]
+    runs-on: ubuntu-latest
+    steps:
+      - name: succeed
+        run: |
+          echo "Success: Required build and lint checks completed!"
+
   final:
     name: Post-CI job (fork)
     if: github.event.pull_request.head.repo.fork

.github/workflows/build_status.yml

@@ -468,6 +468,7 @@ import Mathlib.Algebra.GroupWithZero.Pointwise.Finset
 import Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic
 import Mathlib.Algebra.GroupWithZero.Pointwise.Set.Card
 import Mathlib.Algebra.GroupWithZero.Prod
+import Mathlib.Algebra.GroupWithZero.ProdHom
 import Mathlib.Algebra.GroupWithZero.Semiconj
 import Mathlib.Algebra.GroupWithZero.Subgroup
 import Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
@@ -4325,6 +4326,7 @@ import Mathlib.MeasureTheory.Integral.Periodic
 import Mathlib.MeasureTheory.Integral.Pi
 import Mathlib.MeasureTheory.Integral.Prod
 import Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
+import Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal
 import Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
 import Mathlib.MeasureTheory.Integral.SetIntegral
 import Mathlib.MeasureTheory.Integral.SetToL1
@@ -4554,6 +4556,7 @@ import Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic
 import Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
 import Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty
 import Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable
+import Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
 import Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence
 import Mathlib.NumberTheory.ModularForms.Identities
 import Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Mathlib.lean

@@ -201,8 +201,6 @@ theorem mulSingle_op₂ (op : ∀ i, M i → N i → O i) (h : ∀ i, op i 1 1 =
     mulSingle i (op i x₁ x₂) = fun j => op j (mulSingle i x₁ j) (mulSingle i x₂ j) :=
   Eq.symm <| funext <| apply_mulSingle₂ op h i x₁ x₂
 
-variable (f)
-
 @[to_additive]
 theorem mulSingle_injective (i : ι) : Function.Injective (mulSingle i : M i → ∀ i, M i) :=
   Function.update_injective _ i

Mathlib/Algebra/Group/Pi/Basic.lean

@@ -187,8 +187,7 @@ variable [DecidableEq I]
 
 open Pi
 
-variable (f)
-
+variable (f) in
 /-- The one-preserving homomorphism including a single value
 into a dependent family of values, as functions supported at a point.
 
@@ -206,6 +205,11 @@ nonrec def OneHom.mulSingle [∀ i, One <| f i] (i : I) : OneHom (f i) (∀ i, f
 theorem OneHom.mulSingle_apply [∀ i, One <| f i] (i : I) (x : f i) :
     mulSingle f i x = Pi.mulSingle i x := rfl
 
+@[to_additive (attr := simp, norm_cast)]
+theorem OneHom.coe_mulSingle [∀ i, One <| f i] (i : I) :
+    mulSingle f i = Pi.mulSingle (M := f) i := rfl
+
+variable (f) in
 /-- The monoid homomorphism including a single monoid into a dependent family of additive monoids,
 as functions supported at a point.
 
@@ -223,7 +227,9 @@ theorem MonoidHom.mulSingle_apply [∀ i, MulOneClass <| f i] (i : I) (x : f i)
     mulSingle f i x = Pi.mulSingle i x :=
   rfl
 
-variable {f}
+@[to_additive (attr := simp, norm_cast)]
+theorem MonoidHom.coe_mulSingle [∀ i, MulOneClass <| f i] (i : I) :
+    mulSingle f i = Pi.mulSingle (M := f) i := rfl
 
 @[to_additive]
 theorem Pi.mulSingle_sup [∀ i, SemilatticeSup (f i)] [∀ i, One (f i)] (i : I) (x y : f i) :

Mathlib/Algebra/Group/Pi/Lemmas.lean

@@ -214,6 +214,26 @@ instance {β} [CommMonoidWithZero β] : Mul (α →*₀ β) where
     { (f * g : α →* β) with
       map_zero' := by dsimp; rw [map_zero, zero_mul] }
 
+/-- The trivial homomorphism between monoids with zero, sending everything to 1 other than 0. -/
+protected instance one (M₀ N₀ : Type*) [MulZeroOneClass M₀] [MulZeroOneClass N₀]
+    [DecidablePred fun x : M₀ ↦ x = 0] [Nontrivial M₀] [NoZeroDivisors M₀] :
+    One (M₀ →*₀ N₀) where
+  one.toFun x := if x = 0 then 0 else 1
+  one.map_zero' := by simp
+  one.map_one' := by simp
+  one.map_mul' x y := by split_ifs <;> simp_all
+
+@[simp]
+lemma one_apply_zero {M₀ N₀ : Type*} [MulZeroOneClass M₀] [MulZeroOneClass N₀]
+    [DecidablePred fun x : M₀ ↦ x = 0] [Nontrivial M₀] [NoZeroDivisors M₀] :
+    (1 : M₀ →*₀ N₀) 0 = 0 :=
+  if_pos rfl
+
+lemma one_apply_of_ne_zero {M₀ N₀ : Type*} [MulZeroOneClass M₀] [MulZeroOneClass N₀]
+    [DecidablePred fun x : M₀ ↦ x = 0] [Nontrivial M₀] [NoZeroDivisors M₀] {x : M₀} (hx : x ≠ 0) :
+    (1 : M₀ →*₀ N₀) x = 1 :=
+  if_neg hx
+
 end MonoidWithZeroHom
 
 section CommMonoidWithZero

Mathlib/Algebra/GroupWithZero/Hom.lean

@@ -6,6 +6,7 @@ Authors: Eric Wieser, Yaël Dillies
 import Mathlib.Algebra.Group.Prod
 import Mathlib.Algebra.GroupWithZero.Hom
 import Mathlib.Algebra.GroupWithZero.Units.Basic
+import Mathlib.Algebra.GroupWithZero.WithZero
 
 /-!
 # Products of monoids with zero, groups with zero
@@ -49,6 +50,14 @@ instance instCommMonoidWithZero [CommMonoidWithZero M₀] [CommMonoidWithZero N
 
 end Prod
 
+variable (M₀) in
+@[simp]
+lemma WithZero.toMonoidWithZeroHom_withZeroUnitsEquiv [GroupWithZero M₀]
+    [DecidablePred fun x : M₀ ↦ x = 0] :
+    MonoidWithZeroHomClass.toMonoidWithZeroHom WithZero.withZeroUnitsEquiv =
+      WithZero.lift' (Units.coeHom M₀) :=
+  rfl
+
 /-! ### Multiplication and division as homomorphisms -/
 
 section BundledMulDiv