Merge master into nightly-testing

Author: mathlib-nightly-testing[bot]

Mathlib.lean

@@ -3583,6 +3583,7 @@ public import Mathlib.Combinatorics.SimpleGraph.UniversalVerts
 public import Mathlib.Combinatorics.SimpleGraph.VertexCover
 public import Mathlib.Combinatorics.SimpleGraph.Walk
 public import Mathlib.Combinatorics.SimpleGraph.Walk.Basic
+public import Mathlib.Combinatorics.SimpleGraph.Walk.Chord
 public import Mathlib.Combinatorics.SimpleGraph.Walk.Counting
 public import Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
 public import Mathlib.Combinatorics.SimpleGraph.Walk.Maps
@@ -6923,6 +6924,7 @@ public import Mathlib.SetTheory.Lists
 public import Mathlib.SetTheory.Ordinal.Arithmetic
 public import Mathlib.SetTheory.Ordinal.Basic
 public import Mathlib.SetTheory.Ordinal.CantorNormalForm
+public import Mathlib.SetTheory.Ordinal.Commute
 public import Mathlib.SetTheory.Ordinal.Enum
 public import Mathlib.SetTheory.Ordinal.Exponential
 public import Mathlib.SetTheory.Ordinal.Family

Mathlib/Algebra/Algebra/IsSimpleRing.lean

@@ -12,7 +12,7 @@ public import Mathlib.RingTheory.SimpleRing.Basic
 # Facts about algebras when the coefficient ring is a simple ring
 -/
 
-@[expose] public section
+public section
 
 variable (R A : Type*) [CommRing R] [Semiring A] [Algebra R A] [IsSimpleRing R] [Nontrivial A]
 

Mathlib/Algebra/Algebra/Operations.lean

@@ -804,7 +804,7 @@ theorem prod_span {ι : Type*} (s : Finset ι) (M : ι → Set A) :
 
 theorem prod_span_singleton {ι : Type*} (s : Finset ι) (x : ι → A) :
     (∏ i ∈ s, span R ({x i} : Set A)) = span R {∏ i ∈ s, x i} := by
-  rw [prod_span, Set.finset_prod_singleton]
+  rw [prod_span, Set.finsetProd_singleton]
 
 variable (R A)
 
@@ -923,7 +923,7 @@ theorem restrictScalars_image_smul_eq {S M : Type*}
       exact mem_set_smul_of_mem_mem r_in x_in
     · intro r y h h'
       obtain ⟨c, c_supp, hc⟩ := (mem_set_smul ..).mp <| smul_mem _ r h
-      simp only [hc, Finsupp.sum, AddSubmonoidClass.coe_finset_sum, SetLike.val_smul]
+      simp only [hc, Finsupp.sum, AddSubmonoidClass.coe_finsetSum, SetLike.val_smul]
       refine sum_mem fun u u_in ↦ ?_
       obtain ⟨u, u_in', rfl⟩ := c_supp (Finset.mem_coe.mpr u_in)
       rw [algebraMap_smul]

Mathlib/Algebra/Algebra/Rat.lean

@@ -15,7 +15,7 @@ public import Mathlib.Data.Rat.Cast.CharZero
 This file could usefully be split further.
 -/
 
-@[expose] public section
+public section
 
 assert_not_exists Subgroup
 

Mathlib/Algebra/Algebra/Subalgebra/Operations.lean

@@ -41,7 +41,7 @@ variable (S' : Subalgebra R S)
 /-- Suppose we are given `∑ i, lᵢ * sᵢ = 1` ∈ `S`, and `S'` a subalgebra of `S` that contains
 `lᵢ` and `sᵢ`. To check that an `x : S` falls in `S'`, we only need to show that
 `sᵢ ^ n • x ∈ S'` for some `n` for each `sᵢ`. -/
-theorem mem_of_finset_sum_eq_one_of_pow_smul_mem
+theorem mem_of_finsetSum_eq_one_of_pow_smul_mem
     {ι : Type*} (ι' : Finset ι) (s : ι → S) (l : ι → S)
     (e : ∑ i ∈ ι', l i * s i = 1) (hs : ∀ i, s i ∈ S') (hl : ∀ i, l i ∈ S') (x : S)
     (H : ∀ i, ∃ n : ℕ, (s i ^ n : S) • x ∈ S') : x ∈ S' := by
@@ -69,11 +69,14 @@ theorem mem_of_finset_sum_eq_one_of_pow_smul_mem
   refine Submodule.smul_mem _ (⟨_, pow_mem (hs i) _⟩ : S') ?_
   exact ⟨⟨_, hn i⟩, rfl⟩
 
+@[deprecated (since := "2026-04-08")]
+alias mem_of_finset_sum_eq_one_of_pow_smul_mem := mem_of_finsetSum_eq_one_of_pow_smul_mem
+
 theorem mem_of_span_eq_top_of_smul_pow_mem
     (s : Set S) (l : s →₀ S) (hs : Finsupp.linearCombination S ((↑) : s → S) l = 1)
     (hs' : s ⊆ S') (hl : ∀ i, l i ∈ S') (x : S) (H : ∀ r : s, ∃ n : ℕ, (r : S) ^ n • x ∈ S') :
     x ∈ S' :=
-  mem_of_finset_sum_eq_one_of_pow_smul_mem S' l.support (↑) l hs (fun x => hs' x.2) hl x H
+  mem_of_finsetSum_eq_one_of_pow_smul_mem S' l.support (↑) l hs (fun x => hs' x.2) hl x H
 
 end Subalgebra
 

Mathlib/Algebra/Algebra/Subalgebra/Order.lean

@@ -12,7 +12,7 @@ public import Mathlib.Algebra.Ring.Subsemiring.Order
 # Order instances on subalgebras
 -/
 
-@[expose] public section
+public section
 
 namespace Subalgebra
 

Mathlib/Algebra/Azumaya/Basic.lean

@@ -30,7 +30,7 @@ Noncommutative algebra, Azumaya algebra, Brauer Group
 
 -/
 
-@[expose] public section
+public section
 
 open scoped TensorProduct
 

Mathlib/Algebra/Azumaya/Matrix.lean

@@ -20,7 +20,7 @@ is an Azumaya algebra where `R` is a commutative ring.
 
 -/
 
-@[expose] public section
+public section
 open scoped TensorProduct
 
 variable (R n : Type*) [CommSemiring R] [Fintype n] [DecidableEq n]

Mathlib/Algebra/BigOperators/Associated.lean

@@ -160,11 +160,13 @@ variable [CommMonoid M]
 theorem prod_mk {p : Multiset M} : (p.map Associates.mk).prod = Associates.mk p.prod :=
   Multiset.induction_on p (by simp) fun a s ih => by simp [ih, Associates.mk_mul_mk]
 
-theorem finset_prod_mk {p : Finset ι} {f : ι → M} :
+theorem finsetProd_mk {p : Finset ι} {f : ι → M} :
     (∏ i ∈ p, Associates.mk (f i)) = Associates.mk (∏ i ∈ p, f i) := by
   rw [Finset.prod_eq_multiset_prod, ← Function.comp_def, ← Multiset.map_map, prod_mk,
     ← Finset.prod_eq_multiset_prod]
 
+@[deprecated (since := "2026-04-08")] alias finset_prod_mk := finsetProd_mk
+
 theorem rel_associated_iff_map_eq_map {p q : Multiset M} :
     Multiset.Rel Associated p q ↔ p.map Associates.mk = q.map Associates.mk := by
   rw [← Multiset.rel_eq, Multiset.rel_map]
@@ -216,20 +218,24 @@ section CommMonoidWithZero
 
 variable {M : Type*} [CommMonoidWithZero M]
 
-theorem Prime.dvd_finset_prod_iff {S : Finset M₀} {p : M} (pp : Prime p) (g : M₀ → M) :
+theorem Prime.dvd_finsetProd_iff {S : Finset M₀} {p : M} (pp : Prime p) (g : M₀ → M) :
     p ∣ S.prod g ↔ ∃ a ∈ S, p ∣ g a :=
   ⟨pp.exists_mem_finset_dvd, fun ⟨_, ha1, ha2⟩ => dvd_trans ha2 (dvd_prod_of_mem g ha1)⟩
 
-theorem Prime.not_dvd_finset_prod {S : Finset M₀} {p : M} (pp : Prime p) {g : M₀ → M}
+@[deprecated (since := "2026-04-08")] alias Prime.dvd_finset_prod_iff := Prime.dvd_finsetProd_iff
+
+theorem Prime.not_dvd_finsetProd {S : Finset M₀} {p : M} (pp : Prime p) {g : M₀ → M}
     (hS : ∀ a ∈ S, ¬p ∣ g a) : ¬p ∣ S.prod g := by
-  exact mt (Prime.dvd_finset_prod_iff pp _).1 <| not_exists.2 fun a => not_and.2 (hS a)
+  exact mt (Prime.dvd_finsetProd_iff pp _).1 <| not_exists.2 fun a => not_and.2 (hS a)
+
+@[deprecated (since := "2026-04-08")] alias Prime.not_dvd_finset_prod := Prime.not_dvd_finsetProd
 
 theorem Prime.dvd_finsuppProd_iff {f : M₀ →₀ M} {g : M₀ → M → ℕ} {p : ℕ} (pp : Prime p) :
     p ∣ f.prod g ↔ ∃ a ∈ f.support, p ∣ g a (f a) :=
-  Prime.dvd_finset_prod_iff pp _
+  Prime.dvd_finsetProd_iff pp _
 
 theorem Prime.not_dvd_finsuppProd {f : M₀ →₀ M} {g : M₀ → M → ℕ} {p : ℕ} (pp : Prime p)
     (hS : ∀ a ∈ f.support, ¬p ∣ g a (f a)) : ¬p ∣ f.prod g :=
-  Prime.not_dvd_finset_prod pp hS
+  Prime.not_dvd_finsetProd pp hS
 
 end CommMonoidWithZero

Mathlib/Algebra/BigOperators/Fin.lean

@@ -752,7 +752,7 @@ theorem prod_ofFn {n : ℕ} {f : Fin n → M} : (ofFn f).prod = ∏ i, f i :=
 end CommMonoid
 
 @[to_additive]
-theorem alternatingProd_eq_finset_prod {G : Type*} [DivisionCommMonoid G] :
+theorem alternatingProd_eq_finsetProd {G : Type*} [DivisionCommMonoid G] :
     ∀ (L : List G), alternatingProd L = ∏ i : Fin L.length, L[i] ^ (-1 : ℤ) ^ (i : ℕ)
   | [] => by
     rw [alternatingProd, Finset.prod_eq_one]
@@ -763,9 +763,12 @@ theorem alternatingProd_eq_finset_prod {G : Type*} [DivisionCommMonoid G] :
   | g::h::L =>
     calc g * h⁻¹ * L.alternatingProd
       = g * h⁻¹ * ∏ i : Fin L.length, L[i] ^ (-1 : ℤ) ^ (i : ℕ) :=
-        congr_arg _ (alternatingProd_eq_finset_prod _)
+        congr_arg _ (alternatingProd_eq_finsetProd _)
     _ = ∏ i : Fin (L.length + 2), (g::h::L)[i] ^ (-1 : ℤ) ^ (i : ℕ) := by
         { rw [Fin.prod_univ_succ, Fin.prod_univ_succ, mul_assoc]
           simp [pow_add]}
 
+@[deprecated (since := "2026-04-08")]
+alias alternatingProd_eq_finset_prod := alternatingProd_eq_finsetProd
+
 end List