Merge branch 'master' into turan-2

Author: mitchell-horner

Mathlib/Data/Matrix/Basic.lean

@@ -880,4 +880,31 @@ variable {R m α}
 
 end Transpose
 
+section NonUnitalNonAssocSemiring
+variable {ι : Type*} [NonUnitalNonAssocSemiring α] [Fintype n]
+
+theorem sum_mulVec (s : Finset ι) (x : ι → Matrix m n α) (y : n → α) :
+    (∑ i ∈ s, x i) *ᵥ y = ∑ i ∈ s, x i *ᵥ y := by
+  ext
+  simp only [mulVec, dotProduct, sum_apply, Finset.sum_mul, Finset.sum_apply]
+  rw [Finset.sum_comm]
+
+theorem mulVec_sum (x : Matrix m n α) (s : Finset ι) (y : ι → (n → α)) :
+    x *ᵥ ∑ i ∈ s, y i = ∑ i ∈ s, x *ᵥ y i := by
+  ext
+  simp only [mulVec, dotProduct_sum, Finset.sum_apply]
+
+theorem sum_vecMul (s : Finset ι) (x : ι → (n → α)) (y : Matrix n m α) :
+    (∑ i ∈ s, x i) ᵥ* y = ∑ i ∈ s, x i ᵥ* y := by
+  ext
+  simp only [vecMul, sum_dotProduct, Finset.sum_apply]
+
+theorem vecMul_sum (x : n → α) (s : Finset ι) (y : ι → Matrix n m α) :
+    x ᵥ* (∑ i ∈ s, y i) = ∑ i ∈ s, x ᵥ* y i := by
+  ext
+  simp only [vecMul, dotProduct, sum_apply, Finset.mul_sum, Finset.sum_apply]
+  rw [Finset.sum_comm]
+
+end NonUnitalNonAssocSemiring
+
 end Matrix

Mathlib/Data/Matrix/Mul.lean

@@ -138,6 +138,16 @@ theorem dotProduct_comp_equiv_symm (e : n ≃ m) : u ⬝ᵥ x ∘ e.symm = u ∘
 theorem comp_equiv_dotProduct_comp_equiv (e : m ≃ n) : x ∘ e ⬝ᵥ y ∘ e = x ⬝ᵥ y := by
   simp [← dotProduct_comp_equiv_symm, Function.comp_def _ e.symm]
 
+theorem dotProduct_sum {ι : Type*} (u : m → α) (s : Finset ι) (v : ι → (m → α)) :
+    u ⬝ᵥ ∑ i ∈ s, v i = ∑ i ∈ s, u ⬝ᵥ v i := by
+  simp only [dotProduct, Finset.sum_apply, Finset.mul_sum]
+  rw [Finset.sum_comm]
+
+theorem sum_dotProduct {ι : Type*} (s : Finset ι) (u : ι → (m → α)) (v : m → α) :
+    (∑ i ∈ s, u i) ⬝ᵥ v = ∑ i ∈ s, u i ⬝ᵥ v := by
+  simp only [dotProduct, Finset.sum_apply, Finset.sum_mul]
+  rw [Finset.sum_comm]
+
 end NonUnitalNonAssocSemiring
 
 section NonUnitalNonAssocSemiringDecidable

Mathlib/Order/Filter/AtTopBot/Finset.lean

@@ -3,10 +3,12 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Jeremy Avigad, Yury Kudryashov, Patrick Massot
 -/
+import Mathlib.Data.Finset.Order
 import Mathlib.Data.Finset.Preimage
 import Mathlib.Order.Filter.AtTopBot.Tendsto
 import Mathlib.Order.Filter.AtTopBot.Basic
 import Mathlib.Order.Filter.Finite
+import Mathlib.Order.Interval.Finset.Defs
 
 /-!
 # `Filter.atTop` and `Filter.atBot` filters and finite sets.
@@ -70,4 +72,19 @@ theorem tendsto_finset_powerset_atTop_atTop : Tendsto (Finset.powerset (α := α
   refine tendsto_atTop_atTop.mpr fun t ↦ ⟨t.sup id, fun _ hu _ hv ↦ ?_⟩
   exact Finset.mem_powerset.mpr <| (Finset.le_sup_of_le hv fun _ h ↦ h).trans hu
 
+theorem tendsto_finset_Iic_atTop_atTop [Preorder α] [LocallyFiniteOrderBot α] :
+    Tendsto (Finset.Iic (α := α)) atTop atTop := by
+  rcases isEmpty_or_nonempty α with _ | _
+  · exact tendsto_of_isEmpty
+  by_cases h : IsDirected α (· ≤ ·)
+  · refine tendsto_atTop_atTop.mpr fun s ↦ ?_
+    obtain ⟨a, ha⟩ := Finset.exists_le s
+    exact ⟨a, fun b hb c hc ↦ by simpa using (ha c hc).trans hb⟩
+  · obtain h := Filter.atTop_neBot_iff.not.mpr (fun h' ↦ h h'.2)
+    simp [not_ne_iff.mp <| Filter.neBot_iff.not.mp h]
+
+theorem tendsto_finset_Ici_atBot_atTop [Preorder α] [LocallyFiniteOrderTop α] :
+    Tendsto (Finset.Ici (α := α)) atBot atTop :=
+  tendsto_finset_Iic_atTop_atTop (α := αᵒᵈ)
+
 end Filter

Mathlib/RingTheory/LocalRing/Quotient.lean

@@ -106,8 +106,8 @@ lemma basisQuotient_repr {ι} [Fintype ι] (b : Basis ι R S) (x) (i) :
     Ideal.Quotient.mk_smul_mk_quotient_map_quotient, ← Algebra.smul_def]
   rw [← map_sum, Basis.sum_repr b x]
 
-lemma exists_maximalIdeal_pow_le_of_finite_quotient (I : Ideal R) [Finite (R ⧸ I)] :
-    ∃ n, maximalIdeal R ^ n ≤ I := by
+lemma exists_maximalIdeal_pow_le_of_isArtinianRing_quotient
+    (I : Ideal R) [IsArtinianRing (R ⧸ I)] : ∃ n, maximalIdeal R ^ n ≤ I := by
   by_cases hI : I = ⊤
   · simp [hI]
   have : Nontrivial (R ⧸ I) := Ideal.Quotient.nontrivial hI
@@ -122,9 +122,13 @@ lemma exists_maximalIdeal_pow_le_of_finite_quotient (I : Ideal R) [Finite (R ⧸
     Ideal.map_eq_bot_iff_le_ker, Ideal.mk_ker] at hn
   exact ⟨n, hn⟩
 
+@[deprecated (since := "2025-09-27")]
+alias exists_maximalIdeal_pow_le_of_finite_quotient :=
+  exists_maximalIdeal_pow_le_of_isArtinianRing_quotient
+
 lemma finite_quotient_iff [IsNoetherianRing R] [Finite (ResidueField R)] {I : Ideal R} :
     Finite (R ⧸ I) ↔ ∃ n, (maximalIdeal R) ^ n ≤ I := by
-  refine ⟨fun _ ↦ exists_maximalIdeal_pow_le_of_finite_quotient I, ?_⟩
+  refine ⟨fun _ ↦ exists_maximalIdeal_pow_le_of_isArtinianRing_quotient I, ?_⟩
   rintro ⟨n, hn⟩
   have : Finite (R ⧸ maximalIdeal R) := ‹_›
   have := (Ideal.finite_quotient_pow (IsNoetherian.noetherian (maximalIdeal R)) n)

Mathlib/Topology/Algebra/Ring/Compact.lean

@@ -104,7 +104,7 @@ instance finite_residueField_of_compactSpace : Finite (ResidueField R) :=
 lemma isOpen_iff_finite_quotient {I : Ideal R} :
     IsOpen (X := R) I ↔ Finite (R ⧸ I) := by
   refine ⟨AddSubgroup.quotient_finite_of_isOpen I.toAddSubgroup, fun H ↦ ?_⟩
-  obtain ⟨n, hn⟩ := exists_maximalIdeal_pow_le_of_finite_quotient I
+  obtain ⟨n, hn⟩ := exists_maximalIdeal_pow_le_of_isArtinianRing_quotient I
   exact AddSubgroup.isOpen_mono (H₁ := (maximalIdeal R ^ n).toAddSubgroup)
     (H₂ := I.toAddSubgroup) hn (isOpen_maximalIdeal_pow R n)