From 2b4f1fd3b3fd72117ba25a906f40d5021e3b44a6 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Thu, 30 Jul 2026 08:11:18 +0000 Subject: [PATCH 1/8] feat: generalize `range_lt_top_of_det_eq_zero` (#42055) --- Mathlib/LinearAlgebra/Determinant.lean | 16 ++++++---------- 1 file changed, 6 insertions(+), 10 deletions(-) diff --git a/Mathlib/LinearAlgebra/Determinant.lean b/Mathlib/LinearAlgebra/Determinant.lean index b0f09a2f99..8c3b6d97e0 100644 --- a/Mathlib/LinearAlgebra/Determinant.lean +++ b/Mathlib/LinearAlgebra/Determinant.lean @@ -365,17 +365,13 @@ theorem det_eq_zero_iff_ker_ne_bot [IsDomain R] [Free R M] [Module.Finite R M] { rw [← det_toMatrix b, ← Matrix.exists_mulVec_eq_zero_iff] refine ⟨fun i => b.repr v i, by simpa, by simpa [toMatrix_mulVec_repr]⟩ -/-- -If the determinant of a map vanishes, then the map is not onto. -TODO: This should only require `[IsDomain R] [Free R M]`, which we get if we generalize -`Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean`, which includes -`LinearMap.ker_eq_bot_iff_range_eq_top`. --/ -theorem range_lt_top_of_det_eq_zero {𝕜 : Type*} [Field 𝕜] [Module 𝕜 M] {f : M →ₗ[𝕜] M} +/-- If the determinant of a map vanishes, then the map is not onto. -/ +theorem range_lt_top_of_det_eq_zero [IsDomain R] [Free R M] {f : M →ₗ[R] M} (hf : f.det = 0) : range f < ⊤ := by - have : Module.Finite 𝕜 M := by simp [finite_of_det_ne_one (f := f), hf] - rw [lt_top_iff_ne_top, ne_eq, ← ker_eq_bot_iff_range_eq_top, ← ne_eq, ← bot_lt_iff_ne_bot] - exact bot_lt_ker_of_det_eq_zero hf + rw [lt_top_iff_ne_top] + intro h + obtain ⟨g, hg⟩ := f.exists_rightInverse_of_surjective h + simpa [hf] using congr_arg LinearMap.det hg /-- When the function is over the base ring, the determinant is the evaluation at `1`. -/ @[simp] lemma det_ring (f : R →ₗ[R] R) : f.det = f 1 := by From e4c91783ca8e6a7c693ae624ade32fd22d4e43c1 Mon Sep 17 00:00:00 2001 From: Felix Pernegger <188575194+felixpernegger@users.noreply.github.com> Date: Thu, 30 Jul 2026 09:12:33 +0000 Subject: [PATCH 2/8] =?UTF-8?q?chore:=20use=20`=3D=E1=B5=90[=CE=BC]`=20not?= =?UTF-8?q?ation=20more=20(#42263)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Batixx --- Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean | 2 +- Mathlib/MeasureTheory/Integral/Layercake.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean b/Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean index 240e9dcf91..3662f5e003 100644 --- a/Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean +++ b/Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean @@ -1387,7 +1387,7 @@ theorem denseRange_toLpCLM [FiniteDimensional ℝ E] [BorelSpace E] {p : ℝ≥0 refine (mem_closure_iff_nhds_basis Metric.nhds_basis_closedBall).2 fun ε hε ↦ ?_ obtain ⟨g, hg₁, hg₂, hg₃⟩ := MemLp.exist_eLpNorm_sub_le hp hp'.out (Lp.memLp f) hε use (hg₁.toSchwartzMap hg₂).toLp p μ - have : (f : E → F) - ((hg₁.toSchwartzMap hg₂).toLp p μ : E → F) =ᶠ[ae μ] (f : E → F) - g := by + have : (f : E → F) - ((hg₁.toSchwartzMap hg₂).toLp p μ : E → F) =ᵐ[μ] (f : E → F) - g := by filter_upwards [(hg₁.toSchwartzMap hg₂).coeFn_toLp p μ] simp simp only [Set.mem_range, toLpCLM_apply, exists_apply_eq_apply, Metric.mem_closedBall', true_and, diff --git a/Mathlib/MeasureTheory/Integral/Layercake.lean b/Mathlib/MeasureTheory/Integral/Layercake.lean index 15f41be5ce..4f8b92fe2c 100644 --- a/Mathlib/MeasureTheory/Integral/Layercake.lean +++ b/Mathlib/MeasureTheory/Integral/Layercake.lean @@ -290,7 +290,7 @@ theorem lintegral_comp_eq_lintegral_meas_le_mul_of_measurable (μ : Measure α) exists_seq_strictMono_tendsto M have I : ∀ n, g =ᵐ[volume.restrict (Ioc (0 : ℝ) (u n))] 0 := by intro n - obtain ⟨s, hs, uns⟩ : ∃ s, g =ᶠ[ae (Measure.restrict volume (Ioc 0 s))] 0 ∧ u n < s := + obtain ⟨s, hs, uns⟩ : ∃ s, g =ᵐ[Measure.restrict volume (Ioc 0 s)] 0 ∧ u n < s := exists_lt_of_lt_csSup (Set.nonempty_of_mem zero_mem) (uM n) exact ae_restrict_of_ae_restrict_of_subset (Ioc_subset_Ioc_right uns.le) hs have : g =ᵐ[volume.restrict (⋃ n, Ioc (0 : ℝ) (u n))] 0 := (ae_restrict_iUnion_iff _ _).2 I From ccb5ed4c017083b250e5618e8523cfce4d26239d Mon Sep 17 00:00:00 2001 From: Felix Pernegger <188575194+felixpernegger@users.noreply.github.com> Date: Thu, 30 Jul 2026 13:54:46 +0000 Subject: [PATCH 3/8] chore: change docstrings when they should be docComments (#42269) Change `/- ` to `/-- ` when it is arguably meant to be. In a few cases, it wasn't 100% clear to me which is preferable. This was just done with regex search, so probably not exhaustive. Co-authored-by: Batixx --- Mathlib/Algebra/Group/Submonoid/Support.lean | 4 ++-- Mathlib/Algebra/GroupWithZero/Range.lean | 3 ++- Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean | 2 +- Mathlib/CategoryTheory/Adjunction/Mates.lean | 2 +- Mathlib/CategoryTheory/Galois/Basic.lean | 2 +- Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean | 2 +- Mathlib/Order/KrullDimension.lean | 4 ++-- Mathlib/Order/LiminfLimsup.lean | 2 +- Mathlib/Order/OmegaCompletePartialOrder.lean | 3 ++- Mathlib/Order/ScottContinuity/Complete.lean | 2 +- Mathlib/Probability/BrownianMotion/Basic.lean | 2 +- Mathlib/RingTheory/LaurentSeries.lean | 4 ++-- 12 files changed, 17 insertions(+), 15 deletions(-) diff --git a/Mathlib/Algebra/Group/Submonoid/Support.lean b/Mathlib/Algebra/Group/Submonoid/Support.lean index 3b0cf85dae..5fcb000f64 100644 --- a/Mathlib/Algebra/Group/Submonoid/Support.lean +++ b/Mathlib/Algebra/Group/Submonoid/Support.lean @@ -54,8 +54,8 @@ theorem mem_mulSupport {x} : x ∈ M.mulSupport ↔ x ∈ M ∧ x⁻¹ ∈ M := @[to_additive (attr := simp)] theorem mulSupport_toSubmonoid : M.mulSupport.toSubmonoid = M ⊓ M⁻¹ := rfl -@[to_additive] -/- The support of a submonoid is the largest subgroup it contains. -/ +/-- The support of a submonoid is the largest subgroup it contains. -/ +@[to_additive /-- The support of a submonoid is the largest subgroup it contains. -/] theorem _root_.Subgroup.gc_toSubmonoid_mulSupport : GaloisConnection (α := Subgroup G) Subgroup.toSubmonoid mulSupport := fun _ _ ↦ ⟨fun _ _ ↦ by aesop, fun h _ hx ↦ (h hx).1⟩ diff --git a/Mathlib/Algebra/GroupWithZero/Range.lean b/Mathlib/Algebra/GroupWithZero/Range.lean index c656abccc9..41eb80908b 100644 --- a/Mathlib/Algebra/GroupWithZero/Range.lean +++ b/Mathlib/Algebra/GroupWithZero/Range.lean @@ -176,7 +176,8 @@ noncomputable section GroupWithZero variable [GroupWithZero A] [GroupWithZero B] {f : A →*₀ B} -/- When the *domain* is itself a group with zero, the `valueMonoid` and the `valueGroup` coincide.-/ +/-- +When the *domain* is itself a group with zero, the `valueMonoid` and the `valueGroup` coincide. -/ lemma valueMonoid_eq_valueGroup : (valueMonoid f) = (valueGroup f).toSubmonoid := by rw [valueGroup_def, Subgroup.closure_toSubmonoid, Eq.comm] apply Submonoid.closure_eq_of_le diff --git a/Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean b/Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean index 8f444fe996..42fc290416 100644 --- a/Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean +++ b/Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean @@ -239,7 +239,7 @@ lemma hasSum_weierstrassPExcept (l₀ : ℂ) (z : ℂ) : (℘[L - l₀] z) := (L.hasSumLocallyUniformly_weierstrassPExcept l₀).hasSum -/- `weierstrassPExcept l₀` is differentiable on non-lattice points and `l₀`. -/ +/-- `weierstrassPExcept l₀` is differentiable on non-lattice points and `l₀`. -/ lemma differentiableOn_weierstrassPExcept (l₀ : ℂ) : DifferentiableOn ℂ ℘[L - l₀] (L.lattice \ {l₀})ᶜ := by refine (L.hasSumLocallyUniformly_weierstrassPExcept l₀).hasSumLocallyUniformlyOn.differentiableOn diff --git a/Mathlib/CategoryTheory/Adjunction/Mates.lean b/Mathlib/CategoryTheory/Adjunction/Mates.lean index a46895413d..6e603086cb 100644 --- a/Mathlib/CategoryTheory/Adjunction/Mates.lean +++ b/Mathlib/CategoryTheory/Adjunction/Mates.lean @@ -132,7 +132,7 @@ theorem mateEquiv_counit_symm (α : TwoSquare R₁ H G R₂) (d : D) : exact (mateEquiv_counit adj₁ adj₂ ((mateEquiv adj₁ adj₂).symm α) d) set_option backward.defeqAttrib.useBackward true in -/- A component of a transposed version of the mates correspondence. -/ +/-- A component of a transposed version of the mates correspondence. -/ theorem unit_mateEquiv (α : TwoSquare G L₁ L₂ H) (c : C) : G.map (adj₁.unit.app c) ≫ (mateEquiv adj₁ adj₂ α).app _ = adj₂.unit.app _ ≫ R₂.map (α.app _) := by diff --git a/Mathlib/CategoryTheory/Galois/Basic.lean b/Mathlib/CategoryTheory/Galois/Basic.lean index caa99925ca..36a41aab86 100644 --- a/Mathlib/CategoryTheory/Galois/Basic.lean +++ b/Mathlib/CategoryTheory/Galois/Basic.lean @@ -330,7 +330,7 @@ lemma epi_of_nonempty_of_isConnected {X A : C} [IsConnected A] [h : Nonempty (F. lemma surjective_on_fiber_of_epi {X Y : C} (f : X ⟶ Y) [Epi f] : Function.Surjective (F.map f) := surjective_of_epi (FintypeCat.incl.map (F.map f)) -/- A morphism from an object with non-empty fiber to a connected object is surjective on fibers. -/ +/-- A morphism from an object with non-empty fiber to a connected object is surjective on fibers. -/ lemma surjective_of_nonempty_fiber_of_isConnected {X A : C} [Nonempty (F.obj X)] [IsConnected A] (f : X ⟶ A) : Function.Surjective (F.map f) := by diff --git a/Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean b/Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean index d01d85c505..ada6574d2e 100644 --- a/Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean +++ b/Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean @@ -314,7 +314,7 @@ lemma isStrongFEPair_toStrongFEPair : IsStrongFEPair P.toStrongFEPair where hf₀ := rfl hg₀ := rfl -/- Alternative form for the difference between `f - f₀` and its modified term. -/ +/-- Alternative form for the difference between `f - f₀` and its modified term. -/ lemma f_modif_aux1 : EqOn (fun x ↦ P.f_modif x - P.f x + P.f₀) ((Ioo 0 1).indicator (fun x : ℝ ↦ P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) + ({1} : Set ℝ).indicator (fun _ ↦ P.f₀ - P.f 1)) (Ioi 0) := by diff --git a/Mathlib/Order/KrullDimension.lean b/Mathlib/Order/KrullDimension.lean index 5d637a67b8..fdedd76366 100644 --- a/Mathlib/Order/KrullDimension.lean +++ b/Mathlib/Order/KrullDimension.lean @@ -277,7 +277,7 @@ private lemma height_add_const (a : α) (n : ℕ∞) : have hne : Nonempty { p : LTSeries α // p.last = a } := ⟨RelSeries.singleton _ a, rfl⟩ rw [height_eq_iSup_last_eq, iSup_subtype', iSup_subtype', ENat.iSup_add] -/- For elements of finite height, `height` is strictly monotone. -/ +/-- For elements of finite height, `height` is strictly monotone. -/ @[gcongr] lemma height_strictMono {x y : α} (hxy : x < y) (hfin : height x < ⊤) : height x < height y := by rw [← ENat.add_one_le_iff hfin.ne, height_add_const, iSup₂_le_iff] @@ -298,7 +298,7 @@ lemma height_add_one_le {a b : α} (hab : a < b) : height a + 1 ≤ height b := gcongr simp [hfin] -/- For elements of finite height, `coheight` is strictly antitone. -/ +/-- For elements of finite height, `coheight` is strictly antitone. -/ @[gcongr] lemma coheight_strictAnti {x y : α} (hyx : y < x) (hfin : coheight x < ⊤) : coheight x < coheight y := height_strictMono (α := αᵒᵈ) hyx hfin diff --git a/Mathlib/Order/LiminfLimsup.lean b/Mathlib/Order/LiminfLimsup.lean index 0294720f9c..d641dd5a6a 100644 --- a/Mathlib/Order/LiminfLimsup.lean +++ b/Mathlib/Order/LiminfLimsup.lean @@ -881,7 +881,7 @@ theorem limsup_le_iff {x : β} (h₁ : f.IsCoboundedUnder (· ≤ ·) u := by is rcases h' with ⟨z, x_z, hz⟩ exact (h z x_z).mono <| fun w hw ↦ (or_iff_left (not_le_of_gt hw)).1 (hz (u w)) -/- A version of `limsup_le_iff` with large inequalities in densely ordered spaces.-/ +/-- A version of `limsup_le_iff` with large inequalities in densely ordered spaces -/ lemma limsup_le_iff' [DenselyOrdered β] {x : β} (h₁ : IsCoboundedUnder (· ≤ ·) f u := by isBoundedDefault) (h₂ : IsBoundedUnder (· ≤ ·) f u := by isBoundedDefault) : diff --git a/Mathlib/Order/OmegaCompletePartialOrder.lean b/Mathlib/Order/OmegaCompletePartialOrder.lean index 83026896b3..099f11bdb9 100644 --- a/Mathlib/Order/OmegaCompletePartialOrder.lean +++ b/Mathlib/Order/OmegaCompletePartialOrder.lean @@ -294,7 +294,8 @@ lemma ωScottContinuous_iff_monotone_map_ωSup : alias ⟨ωScottContinuous.monotone_map_ωSup, ωScottContinuous.of_monotone_map_ωSup⟩ := ωScottContinuous_iff_monotone_map_ωSup -/- A monotone function `f : α →o β` is ωScott continuous if and only if it distributes over ωSup. -/ +/-- +A monotone function `f : α →o β` is ωScott continuous if and only if it distributes over ωSup. -/ lemma ωScottContinuous_iff_map_ωSup_of_orderHom {f : α →o β} : ωScottContinuous f ↔ ∀ c : Chain α, f (ωSup c) = ωSup (c.map f) := by rw [ωScottContinuous_iff_monotone_map_ωSup] diff --git a/Mathlib/Order/ScottContinuity/Complete.lean b/Mathlib/Order/ScottContinuity/Complete.lean index fbb3fa352c..cb7ee9fe4b 100644 --- a/Mathlib/Order/ScottContinuity/Complete.lean +++ b/Mathlib/Order/ScottContinuity/Complete.lean @@ -26,7 +26,7 @@ section CompleteLattice variable [CompleteLattice α] [CompleteLattice β] -/- `f` is Scott continuous if and only if it commutes with `sSup` on directed sets -/ +/-- `f` is Scott continuous if and only if it commutes with `sSup` on directed sets -/ lemma scottContinuous_iff_map_sSup {f : α → β} : ScottContinuous f ↔ ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (· ≤ ·) d → f (sSup d) = sSup (f '' d) where diff --git a/Mathlib/Probability/BrownianMotion/Basic.lean b/Mathlib/Probability/BrownianMotion/Basic.lean index a2cb37d6c0..2ad458612b 100644 --- a/Mathlib/Probability/BrownianMotion/Basic.lean +++ b/Mathlib/Probability/BrownianMotion/Basic.lean @@ -77,7 +77,7 @@ structure IsPreBrownianReal (X : ℝ≥0 → Ω → ℝ) (P : Measure Ω := by v mk' :: hasLaw : ∀ I : Finset ℝ≥0, HasLaw (fun ω ↦ I.restrict (X · ω)) (projectiveFamily I) P -/- A modification of a pre-Brownian is pre-Brownian. -/ +/-- A modification of a pre-Brownian process is pre-Brownian. -/ lemma IsPreBrownianReal.congr {C : ℝ≥0 → Ω → ℝ} (hB : IsPreBrownianReal B P) (h : ∀ t, B t =ᵐ[P] C t) : IsPreBrownianReal C P where diff --git a/Mathlib/RingTheory/LaurentSeries.lean b/Mathlib/RingTheory/LaurentSeries.lean index f167b704b1..858772ec01 100644 --- a/Mathlib/RingTheory/LaurentSeries.lean +++ b/Mathlib/RingTheory/LaurentSeries.lean @@ -501,7 +501,7 @@ theorem valuation_single_zpow (s : ℤ) : · rw [Int.negSucc_eq, ← inv_inj, ← map_inv₀, inv_single, neg_neg, ← Int.natCast_succ, inv_one, ← HahnSeries.ofPowerSeries_X_pow, PowerSeries.coe_pow, valuation_X_pow, exp_neg] -/- The coefficients of a power series vanish in degree strictly less than its valuation. -/ +/-- The coefficients of a power series vanish in degree strictly less than its valuation. -/ theorem coeff_zero_of_lt_intValuation {n d : ℕ} {f : K⟦X⟧} (H : Valued.v (f : K⸨X⸩) ≤ exp (-d : ℤ)) : n < d → coeff n f = 0 := by @@ -511,7 +511,7 @@ theorem coeff_zero_of_lt_intValuation {n d : ℕ} {f : K⟦X⟧} intValuation_le_pow_iff_dvd (PowerSeries.idealX K) f d, PowerSeries.idealX, Ideal.span_singleton_pow, Ideal.span_singleton_dvd_span_singleton_iff_dvd] at H -/- The valuation of a power series is the order of the first non-zero coefficient. -/ +/-- The valuation of a power series is the order of the first non-zero coefficient. -/ theorem intValuation_le_iff_coeff_lt_eq_zero {d : ℕ} (f : K⟦X⟧) : Valued.v (f : K⸨X⸩) ≤ exp (-d : ℤ) ↔ ∀ n : ℕ, n < d → coeff n f = 0 := by From 62f3addadd0f6b58ac6ddd85c0ceec85012d64a9 Mon Sep 17 00:00:00 2001 From: Michael Rothgang <10105016+grunweg@users.noreply.github.com> Date: Thu, 30 Jul 2026 14:46:42 +0000 Subject: [PATCH 4/8] chore: golf using fun_prop (#40019) Partially enabled through #35683. --- Counterexamples/TopologistsSineCurve.lean | 2 +- Mathlib/Analysis/Convex/Contractible.lean | 2 +- .../Condensed/Discrete/LocallyConstant.lean | 4 +-- Mathlib/Condensed/Light/Sequence.lean | 2 +- .../Constructions/Polish/Basic.lean | 2 +- .../Function/SpecialFunctions/Basic.lean | 34 ++++++------------- 6 files changed, 15 insertions(+), 31 deletions(-) diff --git a/Counterexamples/TopologistsSineCurve.lean b/Counterexamples/TopologistsSineCurve.lean index 218afac81a..f1373a7b72 100644 --- a/Counterexamples/TopologistsSineCurve.lean +++ b/Counterexamples/TopologistsSineCurve.lean @@ -111,7 +111,7 @@ is a continuous image of the positive real line). -/ theorem isConnected_T : IsConnected T := by rw [← closure_S] refine (isConnected_Ioi.image _ <| continuousOn_id.prodMk ?_).closure - exact continuous_sin.comp_continuousOn <| continuousOn_inv₀.mono fun _ hx ↦ hx.ne' + fun_prop (discharger := grind) /-! ## `T` is not path-connected diff --git a/Mathlib/Analysis/Convex/Contractible.lean b/Mathlib/Analysis/Convex/Contractible.lean index 83ad22aafc..78b3005642 100644 --- a/Mathlib/Analysis/Convex/Contractible.lean +++ b/Mathlib/Analysis/Convex/Contractible.lean @@ -28,7 +28,7 @@ protected theorem StarConvex.contractibleSpace (h : StarConvex ℝ x s) (hne : s (contractible_iff_id_nullhomotopic s).2 ⟨⟨x, h.mem hne⟩, ⟨⟨⟨fun p ↦ ⟨p.1.1 • x + (1 - p.1.1) • (p.2 : E), ?_⟩, ?_⟩, fun x ↦ by simp, fun x ↦ by simp⟩⟩⟩ · exact h p.2.2 p.1.2.1 (sub_nonneg.2 p.1.2.2) (add_sub_cancel _ _) - · exact Continuous.subtype_mk (by fun_prop) _ + · fun_prop /-- A non-empty convex set is a contractible space. -/ protected theorem Convex.contractibleSpace (hs : Convex ℝ s) (hne : s.Nonempty) : diff --git a/Mathlib/Condensed/Discrete/LocallyConstant.lean b/Mathlib/Condensed/Discrete/LocallyConstant.lean index e30e86dab9..58d06717ae 100644 --- a/Mathlib/Condensed/Discrete/LocallyConstant.lean +++ b/Mathlib/Condensed/Discrete/LocallyConstant.lean @@ -190,9 +190,7 @@ noncomputable def componentHom (a : Fiber (f.comap g.hom.hom)) : simp only [Fiber.mk, Set.mem_preimage, Set.mem_singleton_iff] convert! map_eq_image _ _ x exact map_preimage_eq_image_map _ _ a⟩ - continuous_toFun := by - -- term mode gives "unknown free variable" error. - exact Continuous.subtype_mk (by fun_prop) _ } + continuous_toFun := by fun_prop } lemma incl_comap {S T : (CompHausLike P)ᵒᵖ} (f : LocallyConstant S.unop (Y.obj (op (CompHausLike.of P PUnit.{u + 1})))) diff --git a/Mathlib/Condensed/Light/Sequence.lean b/Mathlib/Condensed/Light/Sequence.lean index 3b9d812f0b..406aff7aa5 100644 --- a/Mathlib/Condensed/Light/Sequence.lean +++ b/Mathlib/Condensed/Light/Sequence.lean @@ -290,7 +290,7 @@ lemma aux {S T : LightProfinite} (π : T ⟶ S ⊗ ℕ∪{∞}) [Epi π] : rwa [← LightProfinite.epi_iff_surjective] · simp [π', pullback.condition] · exact ⟨ConcreteCategory.ofHom ⟨(sectionOfFibreIncl π' σ' hσ'), - (.subtype_mk (.subtype_mk (by fun_prop) _) _)⟩, rfl⟩ + (.subtype_mk (by fun_prop) _)⟩, rfl⟩ · rw [LightProfinite.epi_iff_surjective] exact coverToFun_surjective _ _ hσ hσ' diff --git a/Mathlib/MeasureTheory/Constructions/Polish/Basic.lean b/Mathlib/MeasureTheory/Constructions/Polish/Basic.lean index 9a3f69f3e3..274477f4af 100644 --- a/Mathlib/MeasureTheory/Constructions/Polish/Basic.lean +++ b/Mathlib/MeasureTheory/Constructions/Polish/Basic.lean @@ -576,7 +576,7 @@ if and only if the set is measurable in `Set.range f`. -/ theorem measurableSet_preimage_iff_preimage_val {f : X → Z} [CountablySeparated (range f)] (hf : Measurable f) {s : Set Z} : MeasurableSet (f ⁻¹' s) ↔ MeasurableSet ((↑) ⁻¹' s : Set (range f)) := - have hf' : Measurable (rangeFactorization f) := hf.subtype_mk + have hf' : Measurable (rangeFactorization f) := by fun_prop hf'.measurableSet_preimage_iff_of_surjective (s := Subtype.val ⁻¹' s) rangeFactorization_surjective diff --git a/Mathlib/MeasureTheory/Function/SpecialFunctions/Basic.lean b/Mathlib/MeasureTheory/Function/SpecialFunctions/Basic.lean index cadcb50ba1..00364325dd 100644 --- a/Mathlib/MeasureTheory/Function/SpecialFunctions/Basic.lean +++ b/Mathlib/MeasureTheory/Function/SpecialFunctions/Basic.lean @@ -109,13 +109,8 @@ theorem measurable_cosh : Measurable cosh := continuous_cosh.measurable theorem measurable_arg : Measurable arg := - have A : Measurable fun x : ℂ => Real.arcsin (x.im / ‖x‖) := - Real.measurable_arcsin.comp (measurable_im.div measurable_norm) - have B : Measurable fun x : ℂ => Real.arcsin ((-x).im / ‖x‖) := - Real.measurable_arcsin.comp ((measurable_im.comp measurable_neg).div measurable_norm) - Measurable.ite (isClosed_le continuous_const continuous_re).measurableSet A <| - Measurable.ite (isClosed_le continuous_const continuous_im).measurableSet (B.add_const _) - (B.sub_const _) + Measurable.ite (by measurability) (by fun_prop) <| + Measurable.ite (by measurability) (by fun_prop) (by fun_prop) theorem measurable_log : Measurable log := (measurable_ofReal.comp <| Real.measurable_log.comp measurable_norm).add <| @@ -269,37 +264,28 @@ end ComplexComposition @[fun_prop] protected theorem Measurable.complex_ofReal {α : Type*} {m : MeasurableSpace α} {f : α → ℝ} (hf : Measurable f) : - Measurable fun x ↦ (f x : ℂ) := - Complex.measurable_ofReal.comp hf + Measurable fun x ↦ (f x : ℂ) := by fun_prop @[fun_prop] protected theorem AEMeasurable.complex_ofReal {α : Type*} {m : MeasurableSpace α} {μ : Measure α} {f : α → ℝ} (hf : AEMeasurable f μ) : - AEMeasurable (fun x ↦ (f x : ℂ)) μ := - Complex.measurable_ofReal.comp_aemeasurable hf + AEMeasurable (fun x ↦ (f x : ℂ)) μ := by + fun_prop section PowInstances instance Complex.hasMeasurablePow : MeasurablePow ℂ ℂ := - ⟨Measurable.ite (measurable_fst (measurableSet_singleton 0)) - (Measurable.ite (measurable_snd (measurableSet_singleton 0)) measurable_one measurable_zero) - (measurable_fst.clog.mul measurable_snd).cexp⟩ + ⟨Measurable.ite (by measurability) + (Measurable.ite (by measurability) measurable_one measurable_zero) (by fun_prop)⟩ -instance Real.hasMeasurablePow : MeasurablePow ℝ ℝ := - ⟨Complex.measurable_re.comp <| - (Complex.measurable_ofReal.comp measurable_fst).pow - (Complex.measurable_ofReal.comp measurable_snd)⟩ +instance Real.hasMeasurablePow : MeasurablePow ℝ ℝ := ⟨Complex.measurable_re.comp <| by fun_prop⟩ -instance NNReal.hasMeasurablePow : MeasurablePow ℝ≥0 ℝ := - ⟨(measurable_fst.coe_nnreal_real.pow measurable_snd).subtype_mk⟩ +instance NNReal.hasMeasurablePow : MeasurablePow ℝ≥0 ℝ := ⟨Measurable.subtype_mk (by fun_prop)⟩ instance ENNReal.hasMeasurablePow : MeasurablePow ℝ≥0∞ ℝ := by refine ⟨ENNReal.measurable_of_measurable_nnreal_prod ?_ ?_⟩ · simp_rw [ENNReal.coe_rpow_def] - refine Measurable.ite ?_ measurable_const (measurable_fst.pow measurable_snd).coe_nnreal_ennreal - exact - MeasurableSet.inter (measurable_fst (measurableSet_singleton 0)) - (measurable_snd measurableSet_Iio) + exact Measurable.ite (by measurability) measurable_const (by fun_prop) · simp_rw [ENNReal.top_rpow_def] refine Measurable.ite measurableSet_Ioi measurable_const ?_ exact Measurable.ite (measurableSet_singleton 0) measurable_const measurable_const From 3b3cdbb692938d509d6fb29fc5e50638985aecf1 Mon Sep 17 00:00:00 2001 From: Rao Xiaojia <7247037+raoxiaojia@users.noreply.github.com> Date: Thu, 30 Jul 2026 16:24:28 +0000 Subject: [PATCH 5/8] feat(LinearAlgebra/Matrix): add definitions and theory for the echelon form and pivots of matrices (#42236) We add definitions for the row echelon form and pivots of matrices. We also add some more API about matrix ranks and add abbreviations for upper/lower-triangular matrices based on the current block triangular definition. Co-authored-by: raoxiaojia --- Mathlib.lean | 2 + .../InnerProductSpace/GramSchmidtOrtho.lean | 10 +- Mathlib/LinearAlgebra/Matrix/Block.lean | 27 ++- .../LinearAlgebra/Matrix/Charpoly/Basic.lean | 7 +- .../Matrix/Determinant/Basic.lean | 4 +- .../LinearAlgebra/Matrix/Echelon/Basic.lean | 103 ++++++++++ .../LinearAlgebra/Matrix/Echelon/Pivot.lean | 182 ++++++++++++++++++ .../LinearAlgebra/Matrix/Nondegenerate.lean | 10 + Mathlib/LinearAlgebra/Matrix/Rank.lean | 94 +++++++-- Mathlib/RingTheory/Polynomial/DegreeLT.lean | 2 +- 10 files changed, 416 insertions(+), 25 deletions(-) create mode 100644 Mathlib/LinearAlgebra/Matrix/Echelon/Basic.lean create mode 100644 Mathlib/LinearAlgebra/Matrix/Echelon/Pivot.lean diff --git a/Mathlib.lean b/Mathlib.lean index 3afd48340d..58520b10d3 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -5135,6 +5135,8 @@ public import Mathlib.LinearAlgebra.Matrix.Diagonal public import Mathlib.LinearAlgebra.Matrix.DotProduct public import Mathlib.LinearAlgebra.Matrix.Dual public import Mathlib.LinearAlgebra.Matrix.DualNumber +public import Mathlib.LinearAlgebra.Matrix.Echelon.Basic +public import Mathlib.LinearAlgebra.Matrix.Echelon.Pivot public import Mathlib.LinearAlgebra.Matrix.FiniteDimensional public import Mathlib.LinearAlgebra.Matrix.FixedDetMatrices public import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic diff --git a/Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean b/Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean index 829ac9dff7..7a3f5b9733 100644 --- a/Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean +++ b/Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean @@ -364,14 +364,18 @@ theorem gramSchmidtOrthonormalBasis_inv_triangular' {i j : ι} (hij : i < j) : /-- Given an indexed family `f : ι → E` of vectors in an inner product space `E`, for which the size of the index set is the dimension of `E`, the matrix of coefficients of `f` with respect to the orthonormal basis `gramSchmidtOrthonormalBasis` constructed from `f` is upper-triangular. -/ -theorem gramSchmidtOrthonormalBasis_inv_blockTriangular : - ((gramSchmidtOrthonormalBasis h f).toBasis.toMatrix f).BlockTriangular id := fun _ _ => +theorem gramSchmidtOrthonormalBasis_inv_isUpperTriangular : + ((gramSchmidtOrthonormalBasis h f).toBasis.toMatrix f).IsUpperTriangular := fun _ _ => gramSchmidtOrthonormalBasis_inv_triangular' h f +@[deprecated (since := "2026-07-30")] +alias gramSchmidtOrthonormalBasis_inv_blockTriangular := + gramSchmidtOrthonormalBasis_inv_isUpperTriangular + theorem gramSchmidtOrthonormalBasis_det [DecidableEq ι] : (gramSchmidtOrthonormalBasis h f).toBasis.det f = ∏ i, ⟪gramSchmidtOrthonormalBasis h f i, f i⟫ := by - convert! Matrix.det_of_upperTriangular (gramSchmidtOrthonormalBasis_inv_blockTriangular h f) + convert! Matrix.det_of_isUpperTriangular (gramSchmidtOrthonormalBasis_inv_isUpperTriangular h f) exact ((gramSchmidtOrthonormalBasis h f).repr_apply_apply (f _) _).symm end OrthonormalBasis diff --git a/Mathlib/LinearAlgebra/Matrix/Block.lean b/Mathlib/LinearAlgebra/Matrix/Block.lean index b5c4fdb43f..cf57df9e31 100644 --- a/Mathlib/LinearAlgebra/Matrix/Block.lean +++ b/Mathlib/LinearAlgebra/Matrix/Block.lean @@ -25,7 +25,7 @@ matrices built out of blocks. * `Matrix.det_of_blockTriangular`: the determinant of a block triangular matrix is equal to the product of the determinants of all the blocks -* `Matrix.det_of_upperTriangular` and `Matrix.det_of_lowerTriangular`: the determinant of +* `Matrix.det_of_isUpperTriangular` and `Matrix.det_of_isLowerTriangular`: the determinant of a triangular matrix is the product of the entries along the diagonal ## Tags @@ -61,6 +61,14 @@ variable [Zero R] def BlockTriangular (M : Matrix m m R) (b : m → α) : Prop := ∀ ⦃i j⦄, b j < b i → M i j = 0 +/-- `M` is upper triangular: entries below the diagonal vanish. -/ +abbrev IsUpperTriangular [LT m] (M : Matrix m m R) : Prop := + M.BlockTriangular id + +/-- `M` is lower triangular: entries above the diagonal vanish. -/ +abbrev IsLowerTriangular [LT m] (M : Matrix m m R) : Prop := + M.BlockTriangular toDual + @[simp] protected theorem BlockTriangular.submatrix {f : n → m} (h : M.BlockTriangular b) : (M.submatrix f f).BlockTriangular (b ∘ f) := fun _ _ hij => h hij @@ -85,6 +93,11 @@ protected theorem blockTriangular_transpose_iff {b : m → αᵒᵈ} : @[simp] theorem blockTriangular_zero : BlockTriangular (0 : Matrix m m R) b := fun _ _ _ => rfl +instance decidableBlockTriangular [DecidableEq R] [Fintype m] [DecidableLT α] : + Decidable (M.BlockTriangular b) := + decidable_of_iff (∀ ij : m × m, b ij.2 < b ij.1 → M ij.1 ij.2 = 0) + ⟨fun h i j hij => h (i, j) hij, fun h _ hij => h hij⟩ + end Zero protected theorem BlockTriangular.neg [NegZeroClass R] {M : Matrix m m R} @@ -321,15 +334,19 @@ theorem BlockTriangular.det_fintype [DecidableEq α] [Fintype α] [LinearOrder have : IsEmpty { i // b i = a } := ⟨fun i => ha <| mem_image.2 ⟨i, mem_univ _, i.2⟩⟩ exact det_isEmpty -theorem det_of_upperTriangular [LinearOrder m] (h : M.BlockTriangular id) : +theorem det_of_isUpperTriangular [LinearOrder m] (h : M.IsUpperTriangular) : M.det = ∏ i : m, M i i := by have : DecidableEq R := Classical.decEq _ simp_rw [h.det, image_id, det_toSquareBlock_id] -theorem det_of_lowerTriangular [LinearOrder m] (M : Matrix m m R) (h : M.BlockTriangular toDual) : +@[deprecated (since := "2026-07-30")] alias det_of_upperTriangular := det_of_isUpperTriangular + +theorem det_of_isLowerTriangular [LinearOrder m] (M : Matrix m m R) (h : M.IsLowerTriangular) : M.det = ∏ i : m, M i i := by rw [← det_transpose] - exact det_of_upperTriangular h.transpose + exact det_of_isUpperTriangular h.transpose + +@[deprecated (since := "2026-07-30")] alias det_of_lowerTriangular := det_of_isLowerTriangular open Polynomial @@ -342,7 +359,7 @@ theorem matrixOfPolynomials_blockTriangular {R} [Semiring R] {n : ℕ} (p : Fin theorem det_matrixOfPolynomials {n : ℕ} (p : Fin n → R[X]) (h_deg : ∀ i, (p i).natDegree = i) (h_monic : ∀ i, Monic <| p i) : (Matrix.of (fun (i j : Fin n) => (p j).coeff i)).det = 1 := by - rw [Matrix.det_of_upperTriangular (Matrix.matrixOfPolynomials_blockTriangular p (fun i ↦ + rw [Matrix.det_of_isUpperTriangular (Matrix.matrixOfPolynomials_blockTriangular p (fun i ↦ Nat.le_of_eq (h_deg i)))] convert! prod_const_one with x _ rw [Matrix.of_apply, ← h_deg, coeff_natDegree, (h_monic x).leadingCoeff] diff --git a/Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean b/Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean index c65cd9f453..24a8db834c 100644 --- a/Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean +++ b/Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean @@ -196,9 +196,12 @@ lemma BlockTriangular.charpoly {α : Type*} {b : n → α} [LinearOrder α] (h : M.charpoly = ∏ a ∈ image b univ, (M.toSquareBlock b a).charpoly := by simp only [Matrix.charpoly, h.charmatrix.det, charmatrix_toSquareBlock] -lemma charpoly_of_upperTriangular [LinearOrder n] (M : Matrix n n R) (h : M.BlockTriangular id) : +lemma charpoly_of_isUpperTriangular [LinearOrder n] (M : Matrix n n R) (h : M.IsUpperTriangular) : M.charpoly = ∏ i : n, (X - C (M i i)) := by - simp [charpoly, det_of_upperTriangular h.charmatrix] + simp [charpoly, det_of_isUpperTriangular h.charmatrix] + +@[deprecated (since := "2026-07-30")] +alias charpoly_of_upperTriangular := charpoly_of_isUpperTriangular -- This proof follows http://drorbn.net/AcademicPensieve/2015-12/CayleyHamilton.pdf /-- The **Cayley-Hamilton Theorem**, that the characteristic polynomial of a matrix, diff --git a/Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean b/Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean index 7a1cfad31c..9f47c32c8a 100644 --- a/Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean +++ b/Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean @@ -670,7 +670,7 @@ theorem det_blockDiagonal {o : Type*} [Fintype o] [DecidableEq o] (M : o → Mat set_option backward.isDefEq.respectTransparency false in /-- The determinant of a 2×2 block matrix with the lower-left block equal to zero is the product of the determinants of the diagonal blocks. For the generalization to any number of blocks, see -`Matrix.det_of_upperTriangular`. -/ +`Matrix.det_of_isUpperTriangular`. -/ @[simp] theorem det_fromBlocks_zero₂₁ (A : Matrix m m R) (B : Matrix m n R) (D : Matrix n n R) : (Matrix.fromBlocks A B 0 D).det = A.det * D.det := by @@ -721,7 +721,7 @@ theorem det_fromBlocks_zero₂₁ (A : Matrix m m R) (B : Matrix m n R) (D : Mat /-- The determinant of a 2×2 block matrix with the upper-right block equal to zero is the product of the determinants of the diagonal blocks. For the generalization to any number of blocks, see -`Matrix.det_of_lowerTriangular`. -/ +`Matrix.det_of_isLowerTriangular`. -/ @[simp] theorem det_fromBlocks_zero₁₂ (A : Matrix m m R) (C : Matrix n m R) (D : Matrix n n R) : (Matrix.fromBlocks A 0 C D).det = A.det * D.det := by diff --git a/Mathlib/LinearAlgebra/Matrix/Echelon/Basic.lean b/Mathlib/LinearAlgebra/Matrix/Echelon/Basic.lean new file mode 100644 index 0000000000..ab540d7bd3 --- /dev/null +++ b/Mathlib/LinearAlgebra/Matrix/Echelon/Basic.lean @@ -0,0 +1,103 @@ +/- +Copyright (c) 2026 Rao Xiaojia. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rao Xiaojia +-/ +module + +public import Mathlib.Data.Fintype.Defs +public import Mathlib.LinearAlgebra.Matrix.Defs +public import Mathlib.Order.Defs.LinearOrder +public import Mathlib.Order.RelClasses + +import Mathlib.Order.WellFounded + + +/-! +# Row echelon forms + +This file defines the row echelon form of matrices and the leading entries of their rows. + +## Main definitions + +- `Matrix.IsRowEchelon` expresses that `A` is in row echelon form: an entry of a lower row + vanishes whenever a higher row is zero at every column strictly to its left. +- `Matrix.IsLeadingEntry`: `c : n` is the leading position of row `i` of `A`. +- `Matrix.IsReducedRowEchelon` additionally requires each leading entry to be `1` and the + entries above it to vanish. + +## Tags + +matrix, echelon form + +-/ + +@[expose] public section + +universe v + +variable {m n : Type*} +variable {R : Type v} {A : Matrix m n R} + +namespace Matrix + +variable [Zero R] + +/-- `A` is in row echelon form: for rows `i₁ < i₂`, if the higher row `i₁` is zero at every +column strictly left of `j₂`, then the lower row `i₂` is zero at `j₂`. -/ +def IsRowEchelon [LT m] [LT n] (A : Matrix m n R) : Prop := + ∀ ⦃i₁ i₂⦄, i₁ < i₂ → ∀ ⦃j₂⦄, (∀ j₁ < j₂, A i₁ j₁ = 0) → A i₂ j₂ = 0 + +/-- In an echelon matrix, rows below a zero row are zero. -/ +theorem IsRowEchelon.row_eq_zero_of_lt [LT m] [LT n] {i₁ i₂ : m} (he : A.IsRowEchelon) + (hlt : i₁ < i₂) (h0 : A i₁ = 0) : A i₂ = 0 := by + funext j + exact he hlt fun j₁ _ => congrFun h0 j₁ + +/-! ### Leading entries -/ + +/-- `c` is the leading position of row `i`. -/ +def IsLeadingEntry [LT n] (A : Matrix m n R) (i : m) (c : n) : Prop := + (∀ j < c, A i j = 0) ∧ A i c ≠ 0 + +theorem IsLeadingEntry.row_ne_zero [LT n] {i : m} {c : n} (hc : A.IsLeadingEntry i c) : + A i ≠ 0 := + fun contra => hc.2 (congrFun contra c) + +theorem row_ne_zero_iff_exists_isLeadingEntry [LT n] [WellFoundedLT n] {i : m} : + A i ≠ 0 ↔ ∃ c, A.IsLeadingEntry i c := by + refine ⟨fun h => ?_, fun ⟨c, hc⟩ => hc.row_ne_zero⟩ + obtain ⟨c, hc, hmin⟩ := wellFounded_lt.has_min {j | A i j ≠ 0} <| Function.ne_iff.mp h + refine ⟨c, ?_, hc⟩ + by_contra + aesop + +/-- If column indices have a linear order, then there's at most one leading position per row. -/ +theorem IsLeadingEntry.unique [LinearOrder n] {i : m} {c₁ c₂ : n} + (h₁ : A.IsLeadingEntry i c₁) (h₂ : A.IsLeadingEntry i c₂) : c₁ = c₂ := + le_antisymm (not_lt.mp fun hlt => h₂.2 (h₁.1 c₂ hlt)) (not_lt.mp fun hlt => h₁.2 (h₂.1 c₁ hlt)) + +instance [DecidableEq R] [Fintype n] [LT n] [DecidableLT n] + (A : Matrix m n R) (i : m) (c : n) : Decidable (A.IsLeadingEntry i c) := + decidable_of_iff ((∀ j < c, A i j = 0) ∧ A i c ≠ 0) Iff.rfl + +/-! ### Reduced row echelon form -/ + +/-- `A` is in reduced row echelon form: it is in row echelon form, each leading entry is +`1`, and entries above a leading entry vanish (entries below one vanish by +`isRowEchelon`). -/ +structure IsReducedRowEchelon [LT m] [LT n] [One R] (A : Matrix m n R) : Prop where + isRowEchelon : A.IsRowEchelon + eq_one ⦃i : m⦄ ⦃c : n⦄ (hA : A.IsLeadingEntry i c) : A i c = 1 + eq_zero ⦃i₁ i₂ : m⦄ ⦃c : n⦄ (hlt : i₁ < i₂) (hA : A.IsLeadingEntry i₂ c) : A i₁ c = 0 + +/-- If the row indices have a linear order, then every entry in a pivot column vanishes +except for the pivot. -/ +theorem IsReducedRowEchelon.eq_zero_of_ne_of_isLeadingEntry [LinearOrder m] [LT n] [One R] + {i₁ i₂ : m} {c : n} (hA : A.IsReducedRowEchelon) (hne : i₁ ≠ i₂) + (hlead : A.IsLeadingEntry i₂ c) : A i₁ c = 0 := by + rcases hne.lt_or_gt with hlt | hlt + · exact hA.eq_zero hlt hlead + · exact hA.isRowEchelon hlt hlead.1 + +end Matrix diff --git a/Mathlib/LinearAlgebra/Matrix/Echelon/Pivot.lean b/Mathlib/LinearAlgebra/Matrix/Echelon/Pivot.lean new file mode 100644 index 0000000000..2224c13b7f --- /dev/null +++ b/Mathlib/LinearAlgebra/Matrix/Echelon/Pivot.lean @@ -0,0 +1,182 @@ +/- +Copyright (c) 2026 Rao Xiaojia. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rao Xiaojia +-/ +module + +public import Mathlib.LinearAlgebra.Matrix.Echelon.Basic +public import Mathlib.LinearAlgebra.Matrix.Rank +public import Mathlib.Order.WithBot + +/-! +# Pivots of a matrix + +`Matrix.IsPivotedBy A l` defines a map-based representation `l` for the pivot, stating that +`l i` is the pivot column of each row `i` of `A`, with `⊤` for a zero row. + +## Main definitions + +- `Matrix.IsPivotedBy`: `l i : WithTop n` is the pivot column of each row `i` of `A`. + +## Main results + +- `Matrix.IsPivotedBy.rank_eq`: the rank of a matrix is its number of pivots. +- `Matrix.IsPivotedBy.unique`: the pivot of a matrix is unique if the column indices have a + linear order. +- `Matrix.isPivotedBy_iff`: the map-structural characterisation of pivots. + +## Tags + +matrix, echelon form, pivot +-/ + +@[expose] public section + +namespace Matrix + +open Finset + +variable {m n : Type*} {R : Type*} + +section Zero + +variable [Zero R] {A : Matrix m n R} {l : m → WithTop n} + +/-- `A` is in row echelon form and `l i` is the leading position of each row `i`, +with `⊤` for a zero row. -/ +structure IsPivotedBy [LT m] [LT n] (A : Matrix m n R) (l : m → WithTop n) : Prop where + isRowEchelon : A.IsRowEchelon + isPivotEntry (i : m) : + (∀ j : n, (j : WithTop n) < l i → A i j = 0) ∧ ∀ c : n, l i = c → A i c ≠ 0 + +namespace IsPivotedBy + +theorem isLeadingEntry [LT m] [LT n] {i : m} {c : n} (hA : A.IsPivotedBy l) (hc : l i = c) : + A.IsLeadingEntry i c := by + refine ⟨fun j hj => (hA.isPivotEntry i).1 j ?_, (hA.isPivotEntry i).2 c hc⟩ + rw [hc] + exact_mod_cast hj + +theorem eq_top_iff [LT m] [LT n] {i : m} (hA : A.IsPivotedBy l) : + l i = ⊤ ↔ A i = 0 := by + cases hc : l i with + | top => + have h := (hA.isPivotEntry i).1 + rw [hc] at h + simpa [funext_iff] using fun j => h j (WithTop.coe_lt_top j) + | coe c => simpa using fun h0 => (hA.isPivotEntry i).2 c hc (congrFun h0 c) + +variable [LinearOrder n] + +theorem lt_of_lt_of_ne_top [LT m] {i₁ i₂ : m} + (hA : A.IsPivotedBy l) (hlt : i₁ < i₂) (h₁ : l i₁ ≠ ⊤) : l i₁ < l i₂ := by + by_contra! hle + obtain ⟨c₂, hc₂⟩ := WithTop.ne_top_iff_exists.mp (hle.trans_lt h₁.lt_top).ne + refine (hA.isPivotEntry i₂).2 c₂ hc₂.symm (hA.isRowEchelon hlt fun j₁ hj₁ => ?_) + exact (hA.isPivotEntry i₁).1 j₁ ((WithTop.coe_lt_coe.mpr hj₁).trans_le (hc₂.le.trans hle)) + +/-- The pivots of a matrix are unique. -/ +theorem unique [LT m] {l' : m → WithTop n} + (hl : A.IsPivotedBy l) (hl' : A.IsPivotedBy l') : l = l' := by + funext i + cases hc' : l' i with + | top => + rw [hl.eq_top_iff, ← hl'.eq_top_iff] + exact hc' + | coe c' => + cases hc : l i with + | top => + rw [hl.eq_top_iff] at hc + exact absurd (congrFun hc c') (hl'.isLeadingEntry hc').2 + | coe c => exact_mod_cast (hl.isLeadingEntry hc).unique (hl'.isLeadingEntry hc') + +theorem strictMonoOn [Preorder m] (hA : A.IsPivotedBy l) : + StrictMonoOn l {i | l i ≠ ⊤} := + fun _ h₁ _ _ hlt => hA.lt_of_lt_of_ne_top hlt h₁ + +variable [PartialOrder m] + +theorem monotone (hA : A.IsPivotedBy l) : + Monotone l := by + refine monotone_iff_forall_lt.mpr ?_ + intro i₁ i₂ hlt + by_cases h₁ : l i₁ = ⊤ + · simp [hA.eq_top_iff.mpr (hA.isRowEchelon.row_eq_zero_of_lt hlt (hA.eq_top_iff.mp h₁))] + · exact (hA.lt_of_lt_of_ne_top hlt h₁).le + +end IsPivotedBy + +/-- The map-structural characterisation of pivots. This is useful for proving that +a matrix is in row echelon form. -/ +theorem isPivotedBy_iff [PartialOrder m] [LinearOrder n] : + A.IsPivotedBy l ↔ + Monotone l ∧ StrictMonoOn l {i | l i ≠ ⊤} ∧ ∀ i : m, + (∀ j : n, (j : WithTop n) < l i → A i j = 0) ∧ ∀ c : n, l i = c → A i c ≠ 0 := by + refine ⟨fun hA => ⟨hA.monotone, hA.strictMonoOn, hA.isPivotEntry⟩, ?_⟩ + refine fun ⟨hmono, hstrict, hlead⟩ ↦ ⟨fun i₁ i₂ hlt j₂ hz ↦ (hlead i₂).1 j₂ ?_, hlead⟩ + rcases eq_or_ne (l i₂) ⊤ with h₂ | h₂ + · rw [h₂] + exact WithTop.coe_lt_top j₂ + · have h₁ : l i₁ ≠ ⊤ := fun ht => h₂ (top_le_iff.mp (ht.symm.le.trans (hmono hlt.le))) + obtain ⟨c₁, hc₁⟩ := WithTop.ne_top_iff_exists.mp h₁ + have hj : (j₂ : WithTop n) ≤ c₁ := + WithTop.coe_le_coe.mpr <| le_of_not_gt fun hgt => (hlead i₁).2 c₁ hc₁.symm (hz c₁ hgt) + exact lt_of_le_of_lt (hj.trans hc₁.le) (hstrict h₁ h₂ hlt) + +/-- A variant of `isPivotedBy_iff` phrased with `Matrix.IsLeadingEntry`. -/ +theorem isPivotedBy_iff' [PartialOrder m] [LinearOrder n] : + A.IsPivotedBy l ↔ + Monotone l ∧ StrictMonoOn l {i | l i ≠ ⊤} ∧ + ∀ i : m, (l i = ⊤ ∧ A i = 0) ∨ (∃ c : n, l i = c ∧ A.IsLeadingEntry i c) := by + rw [isPivotedBy_iff] + refine and_congr_right' <| and_congr_right' <| forall_congr' fun i => ?_ + cases l i <;> simp [IsLeadingEntry, funext_iff] + +end Zero + +section Rank + +variable [Fintype m] [Fintype n] [LinearOrder m] [LinearOrder n] [CommRing R] [IsDomain R] + {A : Matrix m n R} {l : m → WithTop n} + +namespace IsPivotedBy + +theorem rank_eq (hA : A.IsPivotedBy l) : A.rank = #{i | l i ≠ ⊤} := by + refine le_antisymm (A.rank_le_card_of_support_subset _ + (Function.support_subset_iff'.mpr fun i hi => hA.eq_top_iff.mp (by aesop))) ?_ + let g : {i // l i ≠ ⊤} → n := fun i => (l i.1).untop i.2 + have hlead : ∀ i : {i // l i ≠ ⊤}, A.IsLeadingEntry i.1 (g i) := fun i => + hA.isLeadingEntry (WithTop.coe_untop (l i.1) i.2).symm + have htri : (A.submatrix Subtype.val g).IsUpperTriangular := by + intro i j hij + exact (hlead i).1 _ ((WithTop.untop_lt_untop_iff _ _).mpr (hA.strictMonoOn j.2 i.2 hij)) + have hdet : (A.submatrix Subtype.val g).det ≠ 0 := by + rw [det_of_isUpperTriangular htri] + exact prod_ne_zero_iff.mpr fun i _ => (hlead i).2 + calc #{i | l i ≠ ⊤} + = (A.submatrix Subtype.val g).rank := by + rw [rank_of_det_ne_zero hdet, Fintype.card_subtype] + _ ≤ A.rank := rank_submatrix_le A Subtype.val g + +end IsPivotedBy + +end Rank + +/-! ## Decidability -/ + +section Decidability + +variable [Zero R] [DecidableEq R] + +instance [Fintype m] [LinearOrder m] [Fintype n] [LinearOrder n] + (A : Matrix m n R) (l : m → WithTop n) : Decidable (A.IsPivotedBy l) := + -- instance resolution cannot nest `Fintype.decidableForallFintype` under another binder + have : DecidablePred fun i : m => + (∀ j : n, (j : WithTop n) < l i → A i j = 0) ∧ ∀ c : n, l i = c → A i c ≠ 0 := + fun _ => inferInstance + decidable_of_iff' _ isPivotedBy_iff + +end Decidability + +end Matrix diff --git a/Mathlib/LinearAlgebra/Matrix/Nondegenerate.lean b/Mathlib/LinearAlgebra/Matrix/Nondegenerate.lean index 14a74a2c31..c5e738e779 100644 --- a/Mathlib/LinearAlgebra/Matrix/Nondegenerate.lean +++ b/Mathlib/LinearAlgebra/Matrix/Nondegenerate.lean @@ -181,6 +181,16 @@ theorem eq_zero_of_mulVec_eq_zero [NoZeroDivisors R] (hM : M.det ≠ 0) {v : m (hv : M *ᵥ v = 0) : v = 0 := nondegenerate_of_det_ne_zero hM |>.separatingRight.eq_zero_of_mulVec_eq_zero hv +/-- See also `Matrix.mulVec_injective_iff_isUnit` when working over a field. -/ +theorem mulVec_injective_of_det_mem_nonZeroDivisors (hM : M.det ∈ R⁰) : + Function.Injective M.mulVec := + fun _ _ hxy => sub_eq_zero.mp + (eq_zero_of_det_mem_nonZeroDivisors_of_mulVec_eq_zero hM (by rw [mulVec_sub, hxy, sub_self])) + +theorem mulVec_injective_of_det_ne_zero [NoZeroDivisors R] (hM : M.det ≠ 0) : + Function.Injective M.mulVec := + mulVec_injective_of_det_mem_nonZeroDivisors (mem_nonZeroDivisors_of_ne_zero hM) + end Determinant end Matrix diff --git a/Mathlib/LinearAlgebra/Matrix/Rank.lean b/Mathlib/LinearAlgebra/Matrix/Rank.lean index e3213bfcf6..a3385c40b9 100644 --- a/Mathlib/LinearAlgebra/Matrix/Rank.lean +++ b/Mathlib/LinearAlgebra/Matrix/Rank.lean @@ -9,6 +9,7 @@ public import Mathlib.LinearAlgebra.Determinant public import Mathlib.LinearAlgebra.Dimension.OrzechProperty public import Mathlib.LinearAlgebra.Dual.Lemmas public import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas +public import Mathlib.LinearAlgebra.Matrix.Block public import Mathlib.LinearAlgebra.Matrix.Diagonal public import Mathlib.LinearAlgebra.Matrix.DotProduct public import Mathlib.LinearAlgebra.Matrix.Dual @@ -213,25 +214,75 @@ theorem rank_of_isUnit [DecidableEq n] [CommSemiring R] [StrongRankCondition R] obtain ⟨A, rfl⟩ := h exact rank_unit A +theorem rank_of_det_mem_nonZeroDivisors {R : Type*} [CommRing R] [Nontrivial R] + [Fintype m] [DecidableEq m] {A : Matrix m m R} (hA : A.det ∈ nonZeroDivisors R) : + A.rank = Fintype.card m := by + rw [rank, LinearMap.finrank_range_of_inj (mulVec_injective_of_det_mem_nonZeroDivisors hA), + Module.finrank_eq_card_basis (Pi.basisFun R m)] + +theorem rank_of_det_ne_zero {R : Type*} [CommRing R] [IsDomain R] [Fintype m] [DecidableEq m] + {A : Matrix m m R} (h : A.det ≠ 0) : A.rank = Fintype.card m := + rank_of_det_mem_nonZeroDivisors (mem_nonZeroDivisors_of_ne_zero h) + +lemma rank_smul_of_mem_nonZeroDivisors {R : Type*} [CommRing R] {c : R} (B : Matrix m n R) + (hc : c ∈ nonZeroDivisors R) : (c • B).rank = B.rank := by + have hc' : IsSMulRegular R c := isSMulRegular_iff_mem_nonZeroSMulDivisors.mpr hc.1 + have hreg : IsSMulRegular (m → R) c := IsSMulRegular.pi fun _ => hc' + let f := LinearMap.lsmul R (m → R) c + have hcomp : (c • B).mulVecLin = f.comp B.mulVecLin := by aesop + rw [rank, rank, hcomp, LinearMap.range_comp] + exact (Submodule.equivMapOfInjective f hreg _).finrank_eq.symm + +lemma rank_mul_eq_left_of_det_mem_nonZeroDivisors {R : Type*} [CommRing R] [DecidableEq n] + (A : Matrix n n R) (B : Matrix m n R) (hA : A.det ∈ nonZeroDivisors R) : + (B * A).rank = B.rank := by + nontriviality R + refine le_antisymm (rank_mul_le_left B A) ?_ + have key : (B * A) * A.adjugate = A.det • B := by + rw [Matrix.mul_assoc, Matrix.mul_adjugate, Matrix.mul_smul, Matrix.mul_one] + calc B.rank = (A.det • B).rank := (rank_smul_of_mem_nonZeroDivisors B hA).symm + _ = ((B * A) * A.adjugate).rank := by rw [key] + _ ≤ (B * A).rank := rank_mul_le_left _ _ + +lemma rank_mul_eq_left_of_det_ne_zero {R : Type*} [CommRing R] [IsDomain R] [DecidableEq n] + (A : Matrix n n R) (B : Matrix m n R) (h : A.det ≠ 0) : (B * A).rank = B.rank := + rank_mul_eq_left_of_det_mem_nonZeroDivisors A B (mem_nonZeroDivisors_of_ne_zero h) + /-- Right multiplying by an invertible matrix does not change the rank -/ @[simp] lemma rank_mul_eq_left_of_isUnit_det {R : Type*} [CommRing R] [DecidableEq n] (A : Matrix n n R) - (B : Matrix m n R) (hA : IsUnit A.det) : (B * A).rank = B.rank := by - suffices Function.Surjective A.mulVecLin by - rw [rank, mulVecLin_mul, LinearMap.range_comp_of_range_eq_top _ - (LinearMap.range_eq_top.mpr this), ← rank] - intro v - exact ⟨(A⁻¹).mulVecLin v, by simp [mul_nonsing_inv _ hA]⟩ + (B : Matrix m n R) (hA : IsUnit A.det) : (B * A).rank = B.rank := + rank_mul_eq_left_of_det_mem_nonZeroDivisors A B hA.mem_nonZeroDivisors + +lemma rank_mul_eq_right_of_det_mem_nonZeroDivisors {R : Type*} [CommRing R] + [Fintype m] [DecidableEq m] (A : Matrix m m R) (B : Matrix m n R) + (hA : A.det ∈ nonZeroDivisors R) : (A * B).rank = B.rank := by + rw [rank, rank, mulVecLin_mul, LinearMap.range_comp, + ← (Submodule.equivMapOfInjective A.mulVecLin + (mulVec_injective_of_det_mem_nonZeroDivisors hA) _).finrank_eq] + +lemma rank_mul_eq_right_of_det_ne_zero {R : Type*} [CommRing R] [IsDomain R] + [Fintype m] [DecidableEq m] (A : Matrix m m R) (B : Matrix m n R) (h : A.det ≠ 0) : + (A * B).rank = B.rank := + rank_mul_eq_right_of_det_mem_nonZeroDivisors A B (mem_nonZeroDivisors_of_ne_zero h) /-- Left multiplying by an invertible matrix does not change the rank -/ @[simp] lemma rank_mul_eq_right_of_isUnit_det {R : Type*} [CommRing R] [Fintype m] [DecidableEq m] - (A : Matrix m m R) (B : Matrix m n R) (hA : IsUnit A.det) : (A * B).rank = B.rank := by - let b : Basis m R (m → R) := Pi.basisFun R m - replace hA : IsUnit (LinearMap.toMatrix b b A.mulVecLin).det := by - convert! hA; rw [← LinearEquiv.eq_symm_apply]; rfl - have hAB : mulVecLin (A * B) = (LinearEquiv.ofIsUnitDet hA).comp (mulVecLin B) := by ext; simp - rw [rank, rank, hAB, LinearMap.range_comp, LinearEquiv.finrank_map_eq] + (A : Matrix m m R) (B : Matrix m n R) (hA : IsUnit A.det) : (A * B).rank = B.rank := + rank_mul_eq_right_of_det_mem_nonZeroDivisors A B hA.mem_nonZeroDivisors + +lemma rank_mul_eq_right_of_isLowerTriangular {R : Type*} [CommRing R] [IsDomain R] + [Fintype m] [LinearOrder m] (A : Matrix m m R) (B : Matrix m n R) + (hA : A.IsLowerTriangular) (hd : ∀ i, A.diag i ≠ 0) : (A * B).rank = B.rank := by + have hdet : A.det ≠ 0 := by simpa [det_of_isLowerTriangular A hA, Finset.prod_ne_zero_iff] + exact rank_mul_eq_right_of_det_ne_zero A B hdet + +lemma rank_mul_eq_right_of_isUpperTriangular {R : Type*} [CommRing R] [IsDomain R] + [Fintype m] [LinearOrder m] (A : Matrix m m R) (B : Matrix m n R) + (hA : A.IsUpperTriangular) (hd : ∀ i, A.diag i ≠ 0) : (A * B).rank = B.rank := by + have hdet : A.det ≠ 0 := by simpa [det_of_isUpperTriangular hA, Finset.prod_ne_zero_iff] + exact rank_mul_eq_right_of_det_ne_zero A B hdet /-- Taking a subset of the rows and columns reduces the rank. -/ theorem rank_submatrix_le [CommSemiring R] [StrongRankCondition R] [Fintype n₀] (A : Matrix m n R) @@ -320,6 +371,25 @@ theorem rank_le_card_height [Fintype m] [CommSemiring R] [StrongRankCondition R] (A : Matrix m n R) : A.rank ≤ Fintype.card m := (Submodule.finrank_le _).trans (finrank_pi R).le +/-- The rank of a matrix is at most the size of any finset containing all its nonzero rows. -/ +theorem rank_le_card_of_support_subset [CommSemiring R] [StrongRankCondition R] (A : Matrix m n R) + (s : Finset m) (hz : Function.support A.row ⊆ s) : A.rank ≤ s.card := by + rw [Function.support_subset_iff'] at hz + classical + set B : Matrix m {x // x ∈ s} R := Matrix.of fun i a => if (a : m) = i then 1 else 0 with hBdef + have hB : B * A.submatrix Subtype.val id = A := by + ext i j + simp only [hBdef, mul_apply, of_apply, submatrix_apply, id_eq] + by_cases hi : i ∈ s + · rw [Fintype.sum_eq_single (⟨i, hi⟩ : {x // x ∈ s}) + fun a ha => by rw [if_neg fun he => ha (Subtype.ext he), zero_mul], if_pos rfl, one_mul] + · have h0 : A i = 0 := hz i hi + aesop + calc A.rank = (B * A.submatrix Subtype.val id).rank := by rw [hB] + _ ≤ (A.submatrix Subtype.val id).rank := rank_mul_le_right _ _ + _ ≤ Fintype.card {x // x ∈ s} := rank_le_card_height _ + _ = s.card := Fintype.card_coe s + theorem rank_le_height [CommSemiring R] [StrongRankCondition R] {m n : ℕ} (A : Matrix (Fin m) (Fin n) R) : A.rank ≤ m := A.rank_le_card_height.trans (Fintype.card_fin m).le diff --git a/Mathlib/RingTheory/Polynomial/DegreeLT.lean b/Mathlib/RingTheory/Polynomial/DegreeLT.lean index 6a74613781..c0d28c96fa 100644 --- a/Mathlib/RingTheory/Polynomial/DegreeLT.lean +++ b/Mathlib/RingTheory/Polynomial/DegreeLT.lean @@ -179,7 +179,7 @@ noncomputable def taylorLinearEquiv (r : R) (n : ℕ) : R[X]_n ≃ₗ[R] R[X]_n (taylorLinearEquiv r n).toLinearMap.det = 1 := by nontriviality R rw [← LinearMap.det_toMatrix (degreeLT.basis R n), - Matrix.det_of_upperTriangular, Fintype.prod_eq_one] + Matrix.det_of_isUpperTriangular, Fintype.prod_eq_one] · intro i rw [LinearMap.toMatrix_apply, degreeLT.basis_repr, ← natDegree_X_pow (R := R) (i : ℕ)] change (taylor r (degreeLT.basis R n i)).coeff _ = 1 From 190aaa2a4c0e9ff8391bea04ab1d70cb0cabc111 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Thu, 30 Jul 2026 17:51:45 +0000 Subject: [PATCH 6/8] doc(Algebra/Category/Grp): fix after renaming of categories (#42287) --- Mathlib/Algebra/Category/Grp/Basic.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Mathlib/Algebra/Category/Grp/Basic.lean b/Mathlib/Algebra/Category/Grp/Basic.lean index 13e4f84c68..581eb7e953 100644 --- a/Mathlib/Algebra/Category/Grp/Basic.lean +++ b/Mathlib/Algebra/Category/Grp/Basic.lean @@ -259,7 +259,7 @@ attribute [instance] AddCommGrpCat.str CommGrpCat.str initialize_simps_projections AddCommGrpCat (carrier → coe, -str) initialize_simps_projections CommGrpCat (carrier → coe, -str) -/-- `Ab` is an abbreviation for `AddCommGroup`, for the sake of mathematicians' sanity. -/ +/-- `Ab` is an abbreviation for `AddCommGrpCat`, for the sake of mathematicians' sanity. -/ abbrev Ab := AddCommGrpCat namespace CommGrpCat @@ -471,7 +471,7 @@ end CommGrpCat namespace AddCommGrpCat --- Note that because `ℤ : Type 0`, this forces `G : AddCommGroup.{0}`, +-- Note that because `ℤ : Type 0`, this forces `G : AddCommGrpCat.{0}`, -- so we write this explicitly to be clear. -- TODO generalize this, requiring a `ULiftInstances.lean` file /-- Any element of an abelian group gives a unique morphism from `ℤ` sending @@ -504,7 +504,7 @@ def MulEquiv.toGrpIso {X Y : GrpCat} (e : X ≃* Y) : X ≅ Y where hom := GrpCat.ofHom e.toMonoidHom inv := GrpCat.ofHom e.symm.toMonoidHom -/-- Build an isomorphism in the category `AddGroup` from an `AddEquiv` between `AddGroup`s. -/ +/-- Build an isomorphism in the category `AddGrpCat` from an `AddEquiv` between `AddGroup`s. -/ add_decl_doc AddEquiv.toAddGrpIso /-- Build an isomorphism in the category `CommGrpCat` from a `MulEquiv` @@ -525,15 +525,15 @@ namespace CategoryTheory.Iso def groupIsoToMulEquiv {X Y : GrpCat} (i : X ≅ Y) : X ≃* Y := MonoidHom.toMulEquiv i.hom.hom i.inv.hom (by ext; simp) (by ext; simp) -/-- Build an `addEquiv` from an isomorphism in the category `AddGroup` -/ +/-- Build an `addEquiv` from an isomorphism in the category `AddGrpCat` -/ add_decl_doc addGroupIsoToAddEquiv -/-- Build a `MulEquiv` from an isomorphism in the category `CommGroup`. -/ +/-- Build a `MulEquiv` from an isomorphism in the category `CommGrpCat`. -/ @[to_additive (attr := simps!)] def commGroupIsoToMulEquiv {X Y : CommGrpCat} (i : X ≅ Y) : X ≃* Y := MonoidHom.toMulEquiv i.hom.hom i.inv.hom (by ext; simp) (by ext; simp) -/-- Build an `AddEquiv` from an isomorphism in the category `AddCommGroup`. -/ +/-- Build an `AddEquiv` from an isomorphism in the category `AddCommGrpCat`. -/ add_decl_doc addCommGroupIsoToAddEquiv end CategoryTheory.Iso From 2705f824bb8992af68a1f3e311fd0356d0eb15fb Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid <56355248+JovanGerb@users.noreply.github.com> Date: Thu, 30 Jul 2026 20:37:57 +0000 Subject: [PATCH 7/8] chore(Util/CountHeartbeats): deprecate the global `#count_heartbeats` command (#42274) This PR deprecates the global `#count_heartbeats` command. (Not to be confused with `#count_heartbeats in`, which we want to keep). The reason is that `#count_heartbeats` doesn't work in its current implementation. A useful alternative is to use `set_option trace.profiler true` with `set_option trace.profiler.useHeartbeats` true. As discussed in https://leanprover.zulipchat.com/#narrow/channel/263328-triage/topic/issue.20.214.2323905.3A.20linter.2EcountHeartbeats.20is.20broken/with/538006069 --- Mathlib/Util/CountHeartbeats.lean | 14 ++++++++++++-- MathlibTest/Util/CountHeartbeats.lean | 6 ++++++ 2 files changed, 18 insertions(+), 2 deletions(-) diff --git a/Mathlib/Util/CountHeartbeats.lean b/Mathlib/Util/CountHeartbeats.lean index 72c4fe8b66..22ca20328b 100644 --- a/Mathlib/Util/CountHeartbeats.lean +++ b/Mathlib/Util/CountHeartbeats.lean @@ -242,6 +242,8 @@ it looks inside `set_option ... in`, but not, for instance, inside `mutual` bloc There is a convenience notation `#count_heartbeats` that simply sets the linter option to true. -/ +@[deprecated "use `#count_heartbeats in` or `set_option trace.profiler true` with \ + `set_option trace.profiler.useHeartbeats true`" (since := "2026-07-30")] register_option linter.countHeartbeats : Bool := { defValue := false descr := "enable the countHeartbeats linter" @@ -251,6 +253,8 @@ register_option linter.countHeartbeats : Bool := { An option used by the `countHeartbeats` linter: if set to `true`, then the countHeartbeats linter rounds down to the nearest 1000 the heartbeat count. -/ +@[deprecated "use `#count_heartbeats in` or `set_option trace.profiler true` with \ + `set_option trace.profiler.useHeartbeats true`" (since := "2026-07-30")] register_option linter.countHeartbeatsApprox : Bool := { defValue := false descr := "if set to `true`, then the countHeartbeats linter rounds down \ @@ -259,7 +263,9 @@ register_option linter.countHeartbeatsApprox : Bool := { namespace CountHeartbeats -@[inherit_doc Mathlib.Linter.linter.countHeartbeats] +@[inherit_doc Mathlib.Linter.linter.countHeartbeats, +deprecated "use `#count_heartbeats in` or `set_option trace.profiler true` with \ + `set_option trace.profiler.useHeartbeats true`" (since := "2026-07-30")] def countHeartbeatsLinter : Linter where run := withSetOptionIn fun stx ↦ do unless getLinterValue linter.countHeartbeats (← getLinterOptions) do return @@ -280,10 +286,11 @@ def countHeartbeatsLinter : Linter where run := withSetOptionIn fun stx ↦ do | none => for msg in msgs do logInfoAt stx m!"{← msg.toString}" +set_option linter.deprecated false in initialize addLinter countHeartbeatsLinter @[inherit_doc Mathlib.Linter.linter.countHeartbeats] -macro "#count_heartbeats" approx:(&" approximately")? : command => do +macro (name := countHeartbeats) "#count_heartbeats" approx:(&" approximately")? : command => do let approx ← if approx.isSome then `(set_option linter.countHeartbeatsApprox true) else @@ -292,6 +299,9 @@ macro "#count_heartbeats" approx:(&" approximately")? : command => do #[← `(command| set_option linter.countHeartbeats true), approx]⟩ +deprecated_syntax countHeartbeats "use `#count_heartbeats in` or \ + `set_option trace.profiler true` with `set_option trace.profiler.useHeartbeats true`" + (since := "2026-07-30") end CountHeartbeats diff --git a/MathlibTest/Util/CountHeartbeats.lean b/MathlibTest/Util/CountHeartbeats.lean index 33f1107255..044f069bf7 100644 --- a/MathlibTest/Util/CountHeartbeats.lean +++ b/MathlibTest/Util/CountHeartbeats.lean @@ -26,6 +26,12 @@ example (a : Nat) : a = a := rfl section using_count_heartbeats -- sets the `countHeartbeats` both linter option and the `approximate` option to `true` +/-- +warning: syntax 'Mathlib.Linter.CountHeartbeats.countHeartbeats' has been deprecated: use `#count_heartbeats in` or `set_option trace.profiler true` with `set_option trace.profiler.useHeartbeats true` + +Note: This linter can be disabled with `set_option linter.deprecated.syntax false` +-/ +#guard_msgs in #count_heartbeats approximately mutual -- mutual declarations get ignored From f60ac0eb466a8db04f36381155dd58b1a213374e Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 31 Jul 2026 05:53:23 +0000 Subject: [PATCH 8/8] feat: add lemmas about products over Finset.Iio (#39078) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * Mostly useful for `ℕ` * I added the `Finset.Iic` lemmas by symmetry, but I'm happy to remove them if we think they are redundant. --- .../BigOperators/Group/LocallyFinite.lean | 29 +++++++++++++++++++ 1 file changed, 29 insertions(+) diff --git a/Mathlib/Algebra/Order/BigOperators/Group/LocallyFinite.lean b/Mathlib/Algebra/Order/BigOperators/Group/LocallyFinite.lean index 0ccb893cde..160df874e1 100644 --- a/Mathlib/Algebra/Order/BigOperators/Group/LocallyFinite.lean +++ b/Mathlib/Algebra/Order/BigOperators/Group/LocallyFinite.lean @@ -113,6 +113,33 @@ lemma prod_Ico_mul_eq_prod_Ico_add_one (hab : a ≤ b) (f : α → M) : end LocallyFiniteOrder +section LocallyFiniteOrderBot +variable [LocallyFiniteOrderBot α] + +@[to_additive (dont_translate := α)] +lemma prod_Iio_add_one_comm [Add α] [One α] [SuccAddOrder α] [NoMaxOrder α] + (a : α) (f : α → M) : ∏ i < a + 1, f i = f a * (∏ i < a, f i) := by + simp [Iio_add_one_eq_Iic, ← Iio_insert, Finset.prod_insert] + +@[to_additive (dont_translate := α) (attr := simp)] +lemma prod_Iio_add_one [Add α] [One α] [SuccAddOrder α] [NoMaxOrder α] + (a : α) (f : α → M) : ∏ i < a + 1, f i = (∏ i < a, f i) * f a := by + simp_rw [prod_Iio_add_one_comm, mul_comm] + +@[to_additive (dont_translate := α)] +lemma prod_Iic_add_one_comm [Add α] [One α] [SuccAddOrder α] [NoMaxOrder α] + (a : α) (f : α → M) : ∏ i ≤ a + 1, f i = f (a + 1) * (∏ i ≤ a, f i) := by + simp only [← Iio_insert, mem_Iio, lt_self_iff_false, not_false_eq_true, prod_insert, + prod_Iio_add_one_comm] + +@[to_additive (dont_translate := α) (attr := simp)] +lemma prod_Iic_add_one [Add α] [One α] [SuccAddOrder α] [NoMaxOrder α] + (a : α) (f : α → M) : ∏ i ≤ a + 1, f i = (∏ i ≤ a, f i) * f (a + 1) := by + simp_rw [prod_Iic_add_one_comm, mul_comm] + +end LocallyFiniteOrderBot + +section LocallyFiniteOrderTopBot variable [Fintype α] [LocallyFiniteOrderTop α] [LocallyFiniteOrderBot α] @[to_additive] @@ -123,6 +150,8 @@ lemma prod_prod_Ioi_mul_eq_prod_prod_off_diag (f : α → α → M) : rw [prod_sigma', prod_sigma'] refine prod_nbij' (fun i ↦ ⟨i.2, i.1⟩) (fun i ↦ ⟨i.2, i.1⟩) ?_ ?_ ?_ ?_ ?_ <;> simp +end LocallyFiniteOrderTopBot + end LinearOrder set_option backward.isDefEq.respectTransparency false in