feat(LinearAlgebra/Matrix/Block, Analysis/Normed/Algebra/MatrixExponential): add BlockTriangular.pow and BlockTriangular.exp by hakii6 · Pull Request #37006 · leanprover-community/mathlib4

hakii6 · 2026-03-22T23:10:48Z

Summary

Add BlockTriangular.pow and BlockTriangular.exp for proving "det (exp A) = exp (trace A)"

Which part using LLM

The part I used LLM is for

Searching duplicated theorems and lemmas I may missed (I already search them myself first).
Help me handle the "variables and signatures", the "letI" part, some of lemmas and theorems trivial but hard to find the true one.
After I finished, let them helped me check the structure match the disciplines of mathlib.
Check the steps PR match the disciplines of mathlib

Most things above are done by me first, then let them to make sure I'm not missing something.

More context

More context can be found in a topic in "# new member" in Zulip

#new members > (Matrix and NormedSpace.exp) | det (exp A) = exp (trace A)

…-pow-exp

github-actions · 2026-03-22T23:10:59Z

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

github-actions · 2026-03-22T23:11:57Z

PR summary 83b5ecb723

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Topology.Instances.Matrix	1595	1598	+3 (+0.19%)
Mathlib.Analysis.Normed.Algebra.MatrixExponential	2147	2148	+1 (+0.05%)

Import changes for all files

Files	Import difference
369 files `Mathlib.Algebra.Module.ZLattice.Basic` `Mathlib.Algebra.Module.ZLattice.Summable` `Mathlib.Analysis.BoundedVariation` `Mathlib.Analysis.BoxIntegral.Basic` `Mathlib.Analysis.BoxIntegral.DivergenceTheorem` `Mathlib.Analysis.BoxIntegral.Integrability` `Mathlib.Analysis.BoxIntegral.Partition.Measure` `Mathlib.Analysis.BoxIntegral.UnitPartition` `Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap` `Mathlib.Analysis.CStarAlgebra.Matrix` `Mathlib.Analysis.Calculus.AddTorsor.Coord` `Mathlib.Analysis.Calculus.BumpFunction.Basic` `Mathlib.Analysis.Calculus.BumpFunction.InnerProduct` `Mathlib.Analysis.Calculus.BumpFunction.Normed` `Mathlib.Analysis.Calculus.ContDiff.Convolution` `Mathlib.Analysis.Calculus.ContDiff.FiniteDimension` `Mathlib.Analysis.Calculus.Deriv.Abs` `Mathlib.Analysis.Calculus.FDeriv.Measurable` `Mathlib.Analysis.Calculus.FDeriv.Norm` `Mathlib.Analysis.Calculus.Gradient.Basic` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional` `Mathlib.Analysis.Calculus.LineDeriv.Measurable` `Mathlib.Analysis.Calculus.Monotone` `Mathlib.Analysis.Calculus.ParametricIntegral` `Mathlib.Analysis.Calculus.ParametricIntervalIntegral` `Mathlib.Analysis.Complex.Conformal` `Mathlib.Analysis.Complex.Tietze` `Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic` `Mathlib.Analysis.Convex.Birkhoff` `Mathlib.Analysis.Convex.Cone.InnerDual` `Mathlib.Analysis.Convex.Continuous` `Mathlib.Analysis.Convex.DoublyStochasticMatrix` `Mathlib.Analysis.Convex.Integral` `Mathlib.Analysis.Convex.Intrinsic` `Mathlib.Analysis.Convex.Measure` `Mathlib.Analysis.Convolution` `Mathlib.Analysis.Distribution.DerivNotation` `Mathlib.Analysis.Distribution.TemperateGrowth` `Mathlib.Analysis.Fourier.AddCircleMulti` `Mathlib.Analysis.Fourier.AddCircle` `Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality` `Mathlib.Analysis.InnerProductSpace.Adjoint` `Mathlib.Analysis.InnerProductSpace.Calculus` `Mathlib.Analysis.InnerProductSpace.CanonicalTensor` `Mathlib.Analysis.InnerProductSpace.Coalgebra` `Mathlib.Analysis.InnerProductSpace.Dual` `Mathlib.Analysis.InnerProductSpace.EuclideanDist` `Mathlib.Analysis.InnerProductSpace.GramMatrix` `Mathlib.Analysis.InnerProductSpace.Harmonic.Basic` `Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl` `Mathlib.Analysis.InnerProductSpace.Laplacian` `Mathlib.Analysis.InnerProductSpace.LaxMilgram` `Mathlib.Analysis.InnerProductSpace.LinearPMap` `Mathlib.Analysis.InnerProductSpace.MeanErgodic` `Mathlib.Analysis.InnerProductSpace.MulOpposite` `Mathlib.Analysis.InnerProductSpace.NormPow` `Mathlib.Analysis.InnerProductSpace.PiL2` `Mathlib.Analysis.InnerProductSpace.ProdL2` `Mathlib.Analysis.InnerProductSpace.Projection.Basic` `Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional` `Mathlib.Analysis.InnerProductSpace.Projection.Reflection` `Mathlib.Analysis.InnerProductSpace.Projection.Submodule` `Mathlib.Analysis.InnerProductSpace.TensorProduct` `Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology` `Mathlib.Analysis.InnerProductSpace.l2Space` `Mathlib.Analysis.LocallyConvex.Montel` `Mathlib.Analysis.Matrix.Hermitian` `Mathlib.Analysis.Matrix.Normed` `Mathlib.Analysis.Matrix` `Mathlib.Analysis.Normed.Affine.AddTorsorBases` `Mathlib.Analysis.Normed.Affine.AsymptoticCone` `Mathlib.Analysis.Normed.Affine.Convex` `Mathlib.Analysis.Normed.Algebra.MatrixExponential` `Mathlib.Analysis.Normed.Algebra.QuaternionExponential` `Mathlib.Analysis.Normed.Module.Dual` `Mathlib.Analysis.Normed.Module.FiniteDimension` `Mathlib.Analysis.Normed.Module.HahnBanach` `Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn` `Mathlib.Analysis.Normed.Module.WeakDual` `Mathlib.Analysis.ODE.PicardLindelof` `Mathlib.Analysis.PSeriesComplex` `Mathlib.Analysis.Polynomial.Fourier` `Mathlib.Analysis.Quaternion` `Mathlib.Analysis.RCLike.Inner` `Mathlib.Analysis.RCLike.Lemmas` `Mathlib.Analysis.Real.Pi.Irrational` `Mathlib.Analysis.Real.Pi.Leibniz` `Mathlib.Analysis.Real.Pi.Wallis` `Mathlib.Analysis.SpecialFunctions.Complex.Arctan` `Mathlib.Analysis.SpecialFunctions.Complex.LogBounds` `Mathlib.Analysis.SpecialFunctions.Integrability.Basic` `Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic` `Mathlib.Analysis.SpecialFunctions.Integrals.Basic` `Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric` `Mathlib.Analysis.SpecialFunctions.JapaneseBracket` `Mathlib.Analysis.SpecialFunctions.Log.Summable` `Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral` `Mathlib.Analysis.SpecialFunctions.NonIntegrable` `Mathlib.Analysis.SpecialFunctions.Pow.Integral` `Mathlib.Analysis.SpecialFunctions.Stirling` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality` `Mathlib.Analysis.SumIntegralComparisons` `Mathlib.Analysis.VonNeumannAlgebra.Basic` `Mathlib.Combinatorics.Additive.AP.Three.Behrend` `Mathlib.Combinatorics.Additive.Randomisation` `Mathlib.Combinatorics.Extremal.RuzsaSzemeredi` `Mathlib.Dynamics.Ergodic.Action.OfMinimal` `Mathlib.Dynamics.Ergodic.AddCircleAdd` `Mathlib.Dynamics.Ergodic.AddCircle` `Mathlib.Dynamics.Ergodic.Extreme` `Mathlib.Dynamics.Ergodic.RadonNikodym` `Mathlib.Geometry.Diffeology.Basic` `Mathlib.Geometry.Euclidean.Altitude` `Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct` `Mathlib.Geometry.Euclidean.Angle.Unoriented.Projection` `Mathlib.Geometry.Euclidean.Circumcenter` `Mathlib.Geometry.Euclidean.Incenter` `Mathlib.Geometry.Euclidean.Inversion.Calculus` `Mathlib.Geometry.Euclidean.MongePoint` `Mathlib.Geometry.Euclidean.Projection` `Mathlib.Geometry.Euclidean.SignedDist` `Mathlib.Geometry.Euclidean.Sphere.Basic` `Mathlib.Geometry.Euclidean.Sphere.OrthRadius` `Mathlib.Geometry.Euclidean.Sphere.SecondInter` `Mathlib.Geometry.Euclidean.Sphere.Tangent` `Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation` `Mathlib.Geometry.Manifold.Algebra.LieGroup` `Mathlib.Geometry.Manifold.Algebra.Monoid` `Mathlib.Geometry.Manifold.Algebra.SmoothFunctions` `Mathlib.Geometry.Manifold.Algebra.Structures` `Mathlib.Geometry.Manifold.Bordism` `Mathlib.Geometry.Manifold.ContMDiff.Atlas` `Mathlib.Geometry.Manifold.ContMDiff.Basic` `Mathlib.Geometry.Manifold.ContMDiff.Constructions` `Mathlib.Geometry.Manifold.ContMDiff.Defs` `Mathlib.Geometry.Manifold.ContMDiff.NormedSpace` `Mathlib.Geometry.Manifold.ContMDiffMFDeriv` `Mathlib.Geometry.Manifold.ContMDiffMap` `Mathlib.Geometry.Manifold.DerivationBundle` `Mathlib.Geometry.Manifold.Diffeomorph` `Mathlib.Geometry.Manifold.GroupLieAlgebra` `Mathlib.Geometry.Manifold.Immersion` `Mathlib.Geometry.Manifold.Instances.Icc` `Mathlib.Geometry.Manifold.Instances.Real` `Mathlib.Geometry.Manifold.Instances.Sphere` `Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra` `Mathlib.Geometry.Manifold.IntegralCurve.Basic` `Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique` `Mathlib.Geometry.Manifold.IntegralCurve.Transform` `Mathlib.Geometry.Manifold.IntegralCurve.UniformTime` `Mathlib.Geometry.Manifold.IsManifold.ExtChartAt` `Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary` `Mathlib.Geometry.Manifold.LocalDiffeomorph` `Mathlib.Geometry.Manifold.MFDeriv.Atlas` `Mathlib.Geometry.Manifold.MFDeriv.Basic` `Mathlib.Geometry.Manifold.MFDeriv.Defs` `Mathlib.Geometry.Manifold.MFDeriv.FDeriv` `Mathlib.Geometry.Manifold.MFDeriv.NormedSpace` `Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions` `Mathlib.Geometry.Manifold.MFDeriv.Tangent` `Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential` `Mathlib.Geometry.Manifold.Metrizable` `Mathlib.Geometry.Manifold.Notation` `Mathlib.Geometry.Manifold.PoincareConjecture` `Mathlib.Geometry.Manifold.Riemannian.Basic` `Mathlib.Geometry.Manifold.Riemannian.PathELength` `Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace` `Mathlib.Geometry.Manifold.Sheaf.Smooth` `Mathlib.Geometry.Manifold.SmoothEmbedding` `Mathlib.Geometry.Manifold.VectorBundle.Basic` `Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic` `Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion` `Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear` `Mathlib.Geometry.Manifold.VectorBundle.Hom` `Mathlib.Geometry.Manifold.VectorBundle.LocalFrame` `Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable` `Mathlib.Geometry.Manifold.VectorBundle.Pullback` `Mathlib.Geometry.Manifold.VectorBundle.Riemannian` `Mathlib.Geometry.Manifold.VectorBundle.SmoothSection` `Mathlib.Geometry.Manifold.VectorBundle.Tangent` `Mathlib.Geometry.Manifold.VectorBundle.Tensoriality` `Mathlib.Geometry.Manifold.VectorField.LieBracket` `Mathlib.Geometry.Manifold.VectorField.Pullback` `Mathlib.InformationTheory.KullbackLeibler.Basic` `Mathlib.InformationTheory.KullbackLeibler.ChainRule` `Mathlib.InformationTheory.KullbackLeibler.KLFun` `Mathlib.LinearAlgebra.Matrix.Permutation` `Mathlib.LinearAlgebra.Matrix.Stochastic` `Mathlib.LinearAlgebra.Matrix.Swap` `Mathlib.MeasureTheory.Constructions.HaarToSphere` `Mathlib.MeasureTheory.Constructions.UnitInterval` `Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace` `Mathlib.MeasureTheory.Covering.Besicovitch` `Mathlib.MeasureTheory.Covering.DensityTheorem` `Mathlib.MeasureTheory.Covering.Differentiation` `Mathlib.MeasureTheory.Covering.LiminfLimsup` `Mathlib.MeasureTheory.Covering.OneDim` `Mathlib.MeasureTheory.Function.AEEqOfIntegral` `Mathlib.MeasureTheory.Function.AbsolutelyContinuous` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic` `Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen` `Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1` `Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator` `Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner` `Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut` `Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Real` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique` `Mathlib.MeasureTheory.Function.ConditionalLExpectation` `Mathlib.MeasureTheory.Function.ConvergenceInDistribution` `Mathlib.MeasureTheory.Function.FactorsThrough` `Mathlib.MeasureTheory.Function.Intersectivity` `Mathlib.MeasureTheory.Function.JacobianOneDim` `Mathlib.MeasureTheory.Function.Jacobian` `Mathlib.MeasureTheory.Function.L2Space` `Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm` `Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike` `Mathlib.MeasureTheory.Group.AddCircle` `Mathlib.MeasureTheory.Group.FundamentalDomain` `Mathlib.MeasureTheory.Group.GeometryOfNumbers` `Mathlib.MeasureTheory.Group.IntegralConvolution` `Mathlib.MeasureTheory.Group.ModularCharacter` `Mathlib.MeasureTheory.Integral.Asymptotics` `Mathlib.MeasureTheory.Integral.Average` `Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap` `Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus` `Mathlib.MeasureTheory.Integral.Bochner.Set` `Mathlib.MeasureTheory.Integral.Bochner.SumMeasure` `Mathlib.MeasureTheory.Integral.CircleAverage` `Mathlib.MeasureTheory.Integral.CircleIntegral` `Mathlib.MeasureTheory.Integral.CircleTransform` `Mathlib.MeasureTheory.Integral.CurveIntegral.Basic` `Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare` `Mathlib.MeasureTheory.Integral.DivergenceTheorem` `Mathlib.MeasureTheory.Integral.DominatedConvergence` `Mathlib.MeasureTheory.Integral.IntervalAverage` `Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun` `Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic` `Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff` `Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable` `Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral` `Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus` `Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts` `Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm` `Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue` `Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic` `Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope` `Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule` `Mathlib.MeasureTheory.Integral.Layercake` `Mathlib.MeasureTheory.Integral.MeanValue` `Mathlib.MeasureTheory.Integral.Pi` `Mathlib.MeasureTheory.Integral.Prod` `Mathlib.MeasureTheory.Integral.Regular` `Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal` `Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real` `Mathlib.MeasureTheory.Integral.TorusIntegral` `Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv` `Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym` `Mathlib.MeasureTheory.Measure.DiracProba` `Mathlib.MeasureTheory.Measure.FiniteMeasureExt` `Mathlib.MeasureTheory.Measure.FiniteMeasurePi` `Mathlib.MeasureTheory.Measure.FiniteMeasureProd` `Mathlib.MeasureTheory.Measure.FiniteMeasure` `Mathlib.MeasureTheory.Measure.Haar.Disintegration` `Mathlib.MeasureTheory.Measure.Haar.DistribChar` `Mathlib.MeasureTheory.Measure.Haar.Extension` `Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar` `Mathlib.MeasureTheory.Measure.Haar.OfBasis` `Mathlib.MeasureTheory.Measure.Haar.Quotient` `Mathlib.MeasureTheory.Measure.Haar.Unique` `Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd` `Mathlib.MeasureTheory.Measure.Hausdorff` `Mathlib.MeasureTheory.Measure.Lebesgue.Basic` `Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar` `Mathlib.MeasureTheory.Measure.Lebesgue.Integral` `Mathlib.MeasureTheory.Measure.LevyProkhorovMetric` `Mathlib.MeasureTheory.Measure.LogLikelihoodRatio` `Mathlib.MeasureTheory.Measure.Portmanteau` `Mathlib.MeasureTheory.Measure.ProbabilityMeasure` `Mathlib.MeasureTheory.Measure.Prokhorov` `Mathlib.MeasureTheory.Measure.TightNormed` `Mathlib.MeasureTheory.Measure.Tight` `Mathlib.MeasureTheory.Measure.Tilted` `Mathlib.MeasureTheory.Order.UpperLower` `Mathlib.MeasureTheory.SpecificCodomains.Pi` `Mathlib.MeasureTheory.SpecificCodomains.WithLp` `Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue` `Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym` `Mathlib.MeasureTheory.VectorMeasure.WithDensity` `Mathlib.NumberTheory.EulerProduct.ExpLog` `Mathlib.NumberTheory.Harmonic.Bounds` `Mathlib.NumberTheory.LSeries.Basic` `Mathlib.NumberTheory.LSeries.Convergence` `Mathlib.NumberTheory.LSeries.Convolution` `Mathlib.NumberTheory.LSeries.Injectivity` `Mathlib.NumberTheory.LSeries.Linearity` `Mathlib.NumberTheory.Modular` `Mathlib.NumberTheory.SiegelsLemma` `Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart` `Mathlib.NumberTheory.Transcendental.Liouville.Measure` `Mathlib.NumberTheory.WellApproximable` `Mathlib.NumberTheory.ZetaValues` `Mathlib.Probability.BorelCantelli` `Mathlib.Probability.CDF` `Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs` `Mathlib.Probability.CondVar` `Mathlib.Probability.ConditionalExpectation` `Mathlib.Probability.Density` `Mathlib.Probability.Distributions.Binomial` `Mathlib.Probability.Distributions.Poisson.PoissonLimitThm` `Mathlib.Probability.Distributions.SetBernoulli` `Mathlib.Probability.Distributions.TwoValued` `Mathlib.Probability.Distributions.Uniform` `Mathlib.Probability.HasLawExists` `Mathlib.Probability.HasLaw` `Mathlib.Probability.IdentDistribIndep` `Mathlib.Probability.IdentDistrib` `Mathlib.Probability.Independence.BoundedContinuousFunction` `Mathlib.Probability.Independence.Conditional` `Mathlib.Probability.Independence.InfinitePi` `Mathlib.Probability.Independence.Integration` `Mathlib.Probability.Independence.ZeroOne` `Mathlib.Probability.Kernel.CompProdEqIff` `Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous` `Mathlib.Probability.Kernel.Composition.IntegralCompProd` `Mathlib.Probability.Kernel.Composition.RadonNikodym` `Mathlib.Probability.Kernel.CondDistrib` `Mathlib.Probability.Kernel.Condexp` `Mathlib.Probability.Kernel.Disintegration.CDFToKernel` `Mathlib.Probability.Kernel.Disintegration.CondCDF` `Mathlib.Probability.Kernel.Disintegration.Density` `Mathlib.Probability.Kernel.Disintegration.Integral` `Mathlib.Probability.Kernel.Disintegration.StandardBorel` `Mathlib.Probability.Kernel.Disintegration.Unique` `Mathlib.Probability.Kernel.IonescuTulcea.Traj` `Mathlib.Probability.Kernel.MeasurableIntegral` `Mathlib.Probability.Kernel.Posterior` `Mathlib.Probability.Kernel.RadonNikodym` `Mathlib.Probability.Kernel.Representation` `Mathlib.Probability.Kernel.SetIntegral` `Mathlib.Probability.Kernel.WithDensity` `Mathlib.Probability.Martingale.Basic` `Mathlib.Probability.Martingale.BorelCantelli` `Mathlib.Probability.Martingale.Centering` `Mathlib.Probability.Martingale.Convergence` `Mathlib.Probability.Martingale.OptionalSampling` `Mathlib.Probability.Martingale.OptionalStopping` `Mathlib.Probability.Martingale.Upcrossing` `Mathlib.Probability.Moments.Basic` `Mathlib.Probability.Moments.CovarianceBilinDual` `Mathlib.Probability.Moments.Covariance` `Mathlib.Probability.Moments.Variance` `Mathlib.Probability.Notation` `Mathlib.Probability.ProbabilityMassFunction.Integrals` `Mathlib.Probability.Process.Adapted` `Mathlib.Probability.Process.Filtration` `Mathlib.Probability.Process.FiniteDimensionalLaws` `Mathlib.Probability.Process.HittingTime` `Mathlib.Probability.Process.PartitionFiltration` `Mathlib.Probability.Process.Predictable` `Mathlib.Probability.Process.Stopping` `Mathlib.Probability.ProductMeasure` `Mathlib.Probability.StrongLaw` `Mathlib.Topology.CWComplex.Abstract.Basic` `Mathlib.Topology.Category.TopCat.Sphere` `Mathlib.Topology.Compactification.OnePoint.Sphere` `Mathlib.Topology.MetricSpace.HausdorffDimension`	1
`Mathlib.Topology.Instances.Matrix`	3

Declarations diff

+ BlockTriangular.exp
+ BlockTriangular.pow
+ blockTriangularSubalgebra
+ blockTriangularSubsemiring
+ blockTriangular_algebraMap
+ isClosed_setOf_blockTriangular
+ mem_blockTriangularSubalgebra
+ mem_blockTriangularSubsemiring

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

Increase in tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type
8336	1	backward.isDefEq

Current commit 167aaa49fa
Reference commit 83b5ecb723

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

wwylele

Some code style comments

Mathlib/LinearAlgebra/Matrix/Block.lean

Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean

Thanks for the review! I've applied all the suggestions. Co-authored-by: Weiyi Wang <[email protected]>

remove redundant line

Mathlib/LinearAlgebra/Matrix/Block.lean

Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean

Co-authored-by: Snir Broshi <[email protected]>

Mathlib/LinearAlgebra/Matrix/Block.lean

Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean

Co-authored-by: Eric Wieser <[email protected]>

Mathlib/LinearAlgebra/Matrix/Block.lean

Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean

Mathlib/LinearAlgebra/Matrix/Block.lean

Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean

Mathlib/LinearAlgebra/Matrix/Block.lean

Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean

Co-authored-by: Eric Wieser <[email protected]>

Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean

Mathlib/LinearAlgebra/Matrix/Block.lean

Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean

Mathlib/LinearAlgebra/Matrix/Block.lean

Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean

Mathlib/Topology/Instances/Matrix.lean

Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean

hakii6 and others added 3 commits March 22, 2026 17:08

feat: block-triangular-pow-exp

0713c1e

feat: block-triangular-pow-exp

741039b

Merge branch 'leanprover-community:master' into feat/block-triangular…

4437dc1

…-pow-exp

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Mar 22, 2026

b-mehta added the LLM-generated PRs with substantial input from LLMs - review accordingly label Mar 22, 2026

wwylele reviewed Mar 23, 2026

View reviewed changes

hakii6 and others added 2 commits March 23, 2026 10:43

Apply suggestions from code review

d2ccef0

Thanks for the review! I've applied all the suggestions. Co-authored-by: Weiyi Wang <[email protected]>

Update MatrixExponential.lean

bb311d2

remove redundant line

SnirBroshi reviewed Mar 23, 2026

View reviewed changes

style (tactics)

2565bb1

Co-authored-by: Snir Broshi <[email protected]>

hakii6 force-pushed the feat/block-triangular-pow-exp branch from f31cabb to 2565bb1 Compare March 23, 2026 08:50

hakii6 added 2 commits March 23, 2026 16:55

style (line ending)

6341c79

style (line ending)

fd15eca

eric-wieser reviewed Mar 23, 2026

View reviewed changes

Mathlib/LinearAlgebra/Matrix/Block.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Mar 23, 2026

View reviewed changes

Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean Outdated Show resolved Hide resolved

hakii6 and others added 4 commits March 24, 2026 09:44

Update Mathlib/LinearAlgebra/Matrix/Block.lean

b3e13b6

Co-authored-by: Eric Wieser <[email protected]>

style (exceeds 100)

94dedd5

Merge branch 'master' into feat/block-triangular-pow-exp

d4f2768

Merge branch 'master' into feat/block-triangular-pow-exp

a22343f