Merge master into nightly-testing

Author: leanprover-community-mathlib4-bot

Mathlib.lean

@@ -1846,6 +1846,7 @@ import Mathlib.CategoryTheory.Galois.Prorepresentability
 import Mathlib.CategoryTheory.Galois.Topology
 import Mathlib.CategoryTheory.Generator.Abelian
 import Mathlib.CategoryTheory.Generator.Basic
+import Mathlib.CategoryTheory.Generator.Indization
 import Mathlib.CategoryTheory.Generator.Preadditive
 import Mathlib.CategoryTheory.Generator.Presheaf
 import Mathlib.CategoryTheory.Generator.Sheaf

Mathlib/Analysis/Calculus/Deriv/Basic.lean

@@ -658,6 +658,9 @@ theorem deriv_const' : (deriv fun _ : 𝕜 => c) = fun _ => 0 :=
 theorem derivWithin_const : derivWithin (fun _ => c) s = 0 := by
   ext; simp [derivWithin]
 
+@[simp]
+theorem derivWithin_zero : derivWithin (0 : 𝕜 → F) s = 0 := derivWithin_const _ _
+
 end Const
 
 section Continuous

Mathlib/Analysis/Calculus/Deriv/Mul.lean

@@ -246,6 +246,17 @@ theorem derivWithin_mul_const (hc : DifferentiableWithinAt 𝕜 c s x) (d : 𝔸
   · exact (hc.hasDerivWithinAt.mul_const d).derivWithin hxs
   · simp [derivWithin_zero_of_isolated hxs]
 
+lemma derivWithin_mul_const_field (u : 𝕜') :
+    derivWithin (fun y => v y * u) s x = derivWithin v s x * u := by
+  by_cases hv : DifferentiableWithinAt 𝕜 v s x
+  · rw [derivWithin_mul_const hv u]
+  by_cases hu : u = 0
+  · simp [hu]
+  rw [derivWithin_zero_of_not_differentiableWithinAt hv, zero_mul,
+      derivWithin_zero_of_not_differentiableWithinAt]
+  have : v = fun x ↦ (v x * u) * u⁻¹ := by ext; simp [hu]
+  exact fun h_diff ↦ hv <| this ▸ h_diff.mul_const _
+
 theorem deriv_mul_const (hc : DifferentiableAt 𝕜 c x) (d : 𝔸) :
     deriv (fun y => c y * d) x = deriv c x * d :=
   (hc.hasDerivAt.mul_const d).deriv
@@ -284,6 +295,11 @@ theorem derivWithin_const_mul (c : 𝔸) (hd : DifferentiableWithinAt 𝕜 d s x
   · exact (hd.hasDerivWithinAt.const_mul c).derivWithin hxs
   · simp [derivWithin_zero_of_isolated hxs]
 
+lemma derivWithin_const_mul_field (u : 𝕜') :
+    derivWithin (fun y => u * v y) s x = u * derivWithin v s x := by
+  simp_rw [mul_comm u]
+  exact derivWithin_mul_const_field u
+
 theorem deriv_const_mul (c : 𝔸) (hd : DifferentiableAt 𝕜 d x) :
     deriv (fun y => c * d y) x = c * deriv d x :=
   (hd.hasDerivAt.const_mul c).deriv

Mathlib/CategoryTheory/Generator/Indization.lean

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2025 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import Mathlib.CategoryTheory.Generator.Basic
+import Mathlib.CategoryTheory.Limits.Indization.Category
+
+/-!
+# Separating set in the category of ind-objects
+
+We construct a separating set in the category of ind-objects.
+
+## Future work
+
+Once we have constructed zero morphisms in the category of ind-objects, we will be able to show
+that under sufficient conditions, the category of ind-objects has a separating object.
+
+-/
+
+universe v u
+
+namespace CategoryTheory
+
+open Limits
+
+section
+
+variable {C : Type u} [Category.{v} C]
+
+theorem Ind.isSeparating_range_yoneda : IsSeparating (Set.range (Ind.yoneda : C ⥤ _).obj) := by
+  refine fun X Y f g h => (cancel_epi (Ind.colimitPresentationCompYoneda X).hom).1 ?_
+  exact colimit.hom_ext (fun i => by simp [← Category.assoc, h])
+
+end
+
+end CategoryTheory

Mathlib/Data/Fintype/Basic.lean

@@ -1060,11 +1060,7 @@ variable [Fintype α] [DecidableEq β] {f : α → β}
 /-- `bijInv f` is the unique inverse to a bijection `f`. This acts
   as a computable alternative to `Function.invFun`. -/
 def bijInv (f_bij : Bijective f) (b : β) : α :=
-  Fintype.choose (fun a => f a = b)
-    (by
-      rcases f_bij.right b with ⟨a', fa_eq_b⟩
-      rw [← fa_eq_b]
-      exact ⟨a', ⟨rfl, fun a h => f_bij.left h⟩⟩)
+  Fintype.choose (fun a => f a = b) (f_bij.existsUnique b)
 
 theorem leftInverse_bijInv (f_bij : Bijective f) : LeftInverse (bijInv f_bij) f := fun a =>
   f_bij.left (choose_spec (fun a' => f a' = f a) _)

Mathlib/RingTheory/Artinian/Ring.lean

@@ -91,6 +91,26 @@ theorem isField_of_isReduced_of_isLocalRing [IsReduced R] [IsLocalRing R] : IsFi
   (IsArtinianRing.equivPi R).trans (RingEquiv.piUnique _) |>.toMulEquiv.isField
     _ (Ideal.Quotient.field _).toIsField
 
+section IsUnit
+
+open nonZeroDivisors
+
+/-- If an element of an artinian ring is not a zero divisor then it is a unit. -/
+theorem isUnit_of_mem_nonZeroDivisors {a : R} (ha : a ∈ R⁰) : IsUnit a :=
+  IsUnit.isUnit_iff_mulLeft_bijective.mpr <|
+    IsArtinian.bijective_of_injective_endomorphism (LinearMap.mulLeft R a)
+      fun _ _ ↦ (mul_cancel_left_mem_nonZeroDivisors ha).mp
+
+/-- In an artinian ring, an element is a unit iff it is a non-zero-divisor.
+See also `isUnit_iff_mem_nonZeroDivisors_of_finite`.-/
+theorem isUnit_iff_mem_nonZeroDivisors {a : R} : IsUnit a ↔ a ∈ R⁰ :=
+  ⟨IsUnit.mem_nonZeroDivisors, isUnit_of_mem_nonZeroDivisors⟩
+
+theorem isUnit_submonoid_eq : IsUnit.submonoid R = R⁰ := by
+  ext; simp [IsUnit.mem_submonoid_iff, isUnit_iff_mem_nonZeroDivisors]
+
+end IsUnit
+
 section Localization
 
 variable (S : Submonoid R) (L : Type*) [CommSemiring L] [Algebra R L] [IsLocalization S L]