-
Notifications
You must be signed in to change notification settings - Fork 282
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - chore(*): tweak priorities for linear algebra #3840
Conversation
!bench |
Here are the benchmark results for commit 7f72490. Benchmark Metric Change
=============================================================================
+ build elaboration -7.0%
+ build tactic execution -9.3%
+ lint instructions -5.8%
+ lint wall-clock -6.6%
+ ~Mathlib.Algebra.Algebra.Basic instructions -7.7%
+ ~Mathlib.Algebra.Algebra.Subalgebra.Basic instructions -12.6%
+ ~Mathlib.Algebra.Category.ModuleCat.Products instructions -7.0%
+ ~Mathlib.Algebra.CubicDiscriminant instructions -12.4%
+ ~Mathlib.Algebra.GroupPower.Order instructions -5.4%
+ ~Mathlib.Algebra.GroupPower.Ring instructions -7.7%
+ ~Mathlib.Algebra.GroupRingAction.Invariant instructions -18.6%
- ~Mathlib.Algebra.Lie.Basic instructions 5.8%
+ ~Mathlib.Algebra.Module.Equiv instructions -9.6%
+ ~Mathlib.Algebra.Module.Projective instructions -9.6%
- ~Mathlib.Algebra.Polynomial.BigOperators instructions 6.9%
+ ~Mathlib.Algebra.Polynomial.GroupRingAction instructions -6.2%
- ~Mathlib.Algebra.Ring.Units instructions 7.8%
+ ~Mathlib.Algebra.RingQuot instructions -5.1%
+ ~Mathlib.Algebra.Star.CHSH instructions -40.1%
+ ~Mathlib.Analysis.Convex.Exposed instructions -58.9%
+ ~Mathlib.Analysis.LocallyConvex.Bounded instructions -34.0%
+ ~Mathlib.Analysis.LocallyConvex.Polar instructions -46.2%
+ ~Mathlib.Analysis.NormedSpace.ConformalLinearMap instructions -58.2%
+ ~Mathlib.Analysis.NormedSpace.ContinuousLinearMap instructions -83.1%
+ ~Mathlib.Analysis.NormedSpace.LinearIsometry instructions -8.3%
- ~Mathlib.Analysis.NormedSpace.Star.Basic instructions 7.0%
+ ~Mathlib.Analysis.Seminorm instructions -21.6%
+ ~Mathlib.Data.Complex.Determinant instructions -13.0%
+ ~Mathlib.Data.Complex.Module instructions -13.6%
- ~Mathlib.Data.Int.Order.Units instructions 6.4%
+ ~Mathlib.Data.MvPolynomial.CommRing instructions -32.0%
+ ~Mathlib.Data.MvPolynomial.Funext instructions -33.2%
+ ~Mathlib.Data.Nat.Cast.Basic instructions -6.6%
- ~Mathlib.Data.Nat.Factorization.Basic instructions 12.9%
- ~Mathlib.Data.Polynomial.Degree.CardPowDegree instructions 5.3%
- ~Mathlib.Data.Polynomial.Div instructions 6.7%
+ ~Mathlib.Data.Polynomial.Eval instructions -10.0%
+ ~Mathlib.Data.Polynomial.FieldDivision instructions -6.2%
+ ~Mathlib.Data.Polynomial.IntegralNormalization instructions -9.4%
+ ~Mathlib.Data.Polynomial.Module instructions -24.6%
- ~Mathlib.Data.Polynomial.Monomial instructions 8.8%
+ ~Mathlib.Data.Polynomial.PartialFractions instructions -8.6%
+ ~Mathlib.Data.Polynomial.Splits instructions -15.4%
- ~Mathlib.Data.Real.Basic instructions 5.8%
- ~Mathlib.Data.ZMod.Algebra instructions 7.5%
- ~Mathlib.Deprecated.Subring instructions 7.5%
- ~Mathlib.FieldTheory.MvPolynomial instructions 82.2%
+ ~Mathlib.FieldTheory.PerfectClosure instructions -7.3%
- ~Mathlib.FieldTheory.Subfield instructions 18.4%
+ ~Mathlib.FieldTheory.Tower instructions -7.5%
- ~Mathlib.GroupTheory.Perm.Sign instructions 7.5%
+ ~Mathlib.LinearAlgebra.AffineSpace.Combination instructions -12.6%
+ ~Mathlib.LinearAlgebra.AffineSpace.Independent instructions -6.2%
- ~Mathlib.LinearAlgebra.AffineSpace.Midpoint instructions 10.2%
+ ~Mathlib.LinearAlgebra.Determinant instructions -30.7%
+ ~Mathlib.LinearAlgebra.Dimension instructions -30.6%
+ ~Mathlib.LinearAlgebra.DirectSum.TensorProduct instructions -24.5%
+ ~Mathlib.LinearAlgebra.FiniteDimensional instructions -12.0%
+ ~Mathlib.LinearAlgebra.Finrank instructions -9.6%
- ~Mathlib.LinearAlgebra.FinsuppVectorSpace instructions 8.9%
+ ~Mathlib.LinearAlgebra.FreeModule.Determinant instructions -19.3%
+ ~Mathlib.LinearAlgebra.FreeModule.Finite.Matrix instructions -24.6%
+ ~Mathlib.LinearAlgebra.FreeModule.Finite.Rank instructions -8.8%
- ~Mathlib.LinearAlgebra.FreeModule.PID instructions 5.8%
+ ~Mathlib.LinearAlgebra.Lagrange instructions -6.7%
+ ~Mathlib.LinearAlgebra.LinearIndependent instructions -8.6%
- ~Mathlib.LinearAlgebra.Matrix.Adjugate instructions 27.3%
+ ~Mathlib.LinearAlgebra.Matrix.FiniteDimensional instructions -24.7%
+ ~Mathlib.LinearAlgebra.Matrix.MvPolynomial instructions -15.2%
- ~Mathlib.LinearAlgebra.Matrix.NonsingularInverse instructions 9.3%
+ ~Mathlib.LinearAlgebra.Matrix.Polynomial instructions -27.6%
- ~Mathlib.LinearAlgebra.Projection instructions 12.8%
+ ~Mathlib.LinearAlgebra.ProjectiveSpace.Basic instructions -44.3%
- ~Mathlib.LinearAlgebra.Quotient instructions 5.5%
+ ~Mathlib.LinearAlgebra.SModEq instructions -7.5%
+ ~Mathlib.LinearAlgebra.SesquilinearForm instructions -42.2%
+ ~Mathlib.LinearAlgebra.Span instructions -32.7%
+ ~Mathlib.LinearAlgebra.TensorProductBasis instructions -21.8%
+ ~Mathlib.NumberTheory.Basic instructions -38.6%
- ~Mathlib.RingTheory.Adjoin.Fg instructions 11.0%
+ ~Mathlib.RingTheory.EisensteinCriterion instructions -26.6%
+ ~Mathlib.RingTheory.FiniteType instructions -36.4%
+ ~Mathlib.RingTheory.Finiteness instructions -6.4%
+ ~Mathlib.RingTheory.FreeRing instructions -6.3%
+ ~Mathlib.RingTheory.Ideal.AssociatedPrime instructions -30.5%
+ ~Mathlib.RingTheory.Ideal.QuotientOperations instructions -33.8%
+ ~Mathlib.RingTheory.Localization.Basic instructions -7.1%
+ ~Mathlib.RingTheory.Localization.FractionRing instructions -11.4%
+ ~Mathlib.RingTheory.Localization.Integer instructions -34.9%
+ ~Mathlib.RingTheory.Localization.InvSubmonoid instructions -15.7%
+ ~Mathlib.RingTheory.Localization.Module instructions -11.5%
+ ~Mathlib.RingTheory.Localization.NumDen instructions -12.6%
+ ~Mathlib.RingTheory.Localization.Submodule instructions -12.2%
+ ~Mathlib.RingTheory.MvPolynomial.Basic instructions -13.4%
+ ~Mathlib.RingTheory.Polynomial.Basic instructions -28.3%
+ ~Mathlib.RingTheory.Polynomial.Chebyshev instructions -9.8%
+ ~Mathlib.RingTheory.Polynomial.Eisenstein.Basic instructions -23.4%
+ ~Mathlib.RingTheory.Polynomial.ScaleRoots instructions -26.4%
+ ~Mathlib.RingTheory.PrincipalIdealDomain instructions -16.8%
+ ~Mathlib.RingTheory.QuotientNilpotent instructions -33.5%
+ ~Mathlib.RingTheory.ReesAlgebra instructions -5.8%
+ ~Mathlib.RingTheory.SimpleModule instructions -24.5%
+ ~Mathlib.RingTheory.Subring.Pointwise instructions -11.5%
- ~Mathlib.RingTheory.Valuation.Integers instructions 17.6%
+ ~Mathlib.RingTheory.Valuation.Quotient instructions -25.3%
- ~Mathlib.RingTheory.ZMod instructions 6.0%
+ ~Mathlib.Topology.Algebra.Module.Basic instructions -53.0%
+ ~Mathlib.Topology.Algebra.Module.Determinant instructions -58.0%
+ ~Mathlib.Topology.Algebra.Module.Simple instructions -23.0%
+ ~Mathlib.Topology.Algebra.Module.StrongTopology instructions -71.0%
+ ~Mathlib.Topology.Algebra.Module.WeakDual instructions -26.9%
+ ~Mathlib.Topology.Algebra.Polynomial instructions -38.8%
+ ~Mathlib.Topology.Algebra.StarSubalgebra instructions -5.6%
+ ~Mathlib.Topology.Instances.RealVectorSpace instructions -6.6%
- ~Mathlib.Topology.MetricSpace.HausdorffDistance instructions 6.1% There were significant changes against commit 4857a22: Benchmark Metric Change
=============================================================================
+ build branch-misses -5.8%
+ build elaboration -8.0%
+ build tactic execution -9.2%
+ lint instructions -5.7%
+ ~Mathlib.Algebra.Algebra.Basic instructions -7.7%
+ ~Mathlib.Algebra.Algebra.Subalgebra.Basic instructions -12.6%
+ ~Mathlib.Algebra.Category.ModuleCat.Products instructions -7.0%
+ ~Mathlib.Algebra.CubicDiscriminant instructions -12.4%
+ ~Mathlib.Algebra.GroupPower.Order instructions -5.4%
+ ~Mathlib.Algebra.GroupPower.Ring instructions -7.7%
+ ~Mathlib.Algebra.GroupRingAction.Invariant instructions -18.6%
- ~Mathlib.Algebra.Lie.Basic instructions 5.8%
+ ~Mathlib.Algebra.Module.Equiv instructions -9.6%
+ ~Mathlib.Algebra.Module.Projective instructions -9.6%
- ~Mathlib.Algebra.Order.Floor instructions 7.0%
- ~Mathlib.Algebra.Polynomial.BigOperators instructions 7.0%
+ ~Mathlib.Algebra.Polynomial.GroupRingAction instructions -6.2%
- ~Mathlib.Algebra.Ring.Units instructions 7.8%
+ ~Mathlib.Algebra.RingQuot instructions -5.0%
+ ~Mathlib.Algebra.Star.CHSH instructions -40.1%
+ ~Mathlib.Analysis.Convex.Exposed instructions -58.9%
+ ~Mathlib.Analysis.LocallyConvex.Bounded instructions -34.0%
+ ~Mathlib.Analysis.LocallyConvex.Polar instructions -46.2%
+ ~Mathlib.Analysis.NormedSpace.ConformalLinearMap instructions -58.2%
+ ~Mathlib.Analysis.NormedSpace.ContinuousLinearMap instructions -83.1%
+ ~Mathlib.Analysis.NormedSpace.LinearIsometry instructions -8.3%
- ~Mathlib.Analysis.NormedSpace.Star.Basic instructions 7.0%
+ ~Mathlib.Analysis.Seminorm instructions -21.6%
+ ~Mathlib.Data.Complex.Determinant instructions -12.9%
+ ~Mathlib.Data.Complex.Module instructions -13.5%
- ~Mathlib.Data.Int.Order.Units instructions 6.4%
+ ~Mathlib.Data.MvPolynomial.CommRing instructions -32.0%
+ ~Mathlib.Data.MvPolynomial.Funext instructions -33.2%
+ ~Mathlib.Data.Nat.Cast.Basic instructions -6.6%
- ~Mathlib.Data.Nat.Digits instructions 5.6%
- ~Mathlib.Data.Nat.Factorization.Basic instructions 12.9%
- ~Mathlib.Data.Polynomial.Degree.CardPowDegree instructions 5.4%
- ~Mathlib.Data.Polynomial.Div instructions 6.7%
+ ~Mathlib.Data.Polynomial.Eval instructions -10.0%
+ ~Mathlib.Data.Polynomial.FieldDivision instructions -6.2%
+ ~Mathlib.Data.Polynomial.IntegralNormalization instructions -9.3%
+ ~Mathlib.Data.Polynomial.Module instructions -24.6%
- ~Mathlib.Data.Polynomial.Monomial instructions 8.8%
+ ~Mathlib.Data.Polynomial.PartialFractions instructions -8.6%
+ ~Mathlib.Data.Polynomial.Splits instructions -15.5%
- ~Mathlib.Data.Real.Basic instructions 5.8%
+ ~Mathlib.Data.String.Basic instructions -23.7%
- ~Mathlib.Data.ZMod.Algebra instructions 7.6%
- ~Mathlib.Deprecated.Subring instructions 7.4%
- ~Mathlib.FieldTheory.MvPolynomial instructions 82.2%
+ ~Mathlib.FieldTheory.PerfectClosure instructions -7.3%
- ~Mathlib.FieldTheory.Subfield instructions 18.6%
+ ~Mathlib.FieldTheory.Tower instructions -7.5%
- ~Mathlib.GroupTheory.Perm.Sign instructions 7.5%
+ ~Mathlib.LinearAlgebra.AffineSpace.Combination instructions -12.6%
+ ~Mathlib.LinearAlgebra.AffineSpace.Independent instructions -6.2%
- ~Mathlib.LinearAlgebra.AffineSpace.Midpoint instructions 10.2%
+ ~Mathlib.LinearAlgebra.Determinant instructions -30.6%
+ ~Mathlib.LinearAlgebra.Dimension instructions -30.6%
+ ~Mathlib.LinearAlgebra.DirectSum.TensorProduct instructions -24.5%
+ ~Mathlib.LinearAlgebra.FiniteDimensional instructions -11.9%
+ ~Mathlib.LinearAlgebra.Finrank instructions -9.3%
- ~Mathlib.LinearAlgebra.FinsuppVectorSpace instructions 8.9%
+ ~Mathlib.LinearAlgebra.FreeModule.Determinant instructions -19.2%
+ ~Mathlib.LinearAlgebra.FreeModule.Finite.Matrix instructions -24.5%
+ ~Mathlib.LinearAlgebra.FreeModule.Finite.Rank instructions -8.8%
- ~Mathlib.LinearAlgebra.FreeModule.PID instructions 5.3%
+ ~Mathlib.LinearAlgebra.LinearIndependent instructions -8.6%
- ~Mathlib.LinearAlgebra.Matrix.Adjugate instructions 27.3%
+ ~Mathlib.LinearAlgebra.Matrix.FiniteDimensional instructions -24.7%
+ ~Mathlib.LinearAlgebra.Matrix.MvPolynomial instructions -15.1%
- ~Mathlib.LinearAlgebra.Matrix.NonsingularInverse instructions 9.3%
+ ~Mathlib.LinearAlgebra.Matrix.Polynomial instructions -27.6%
- ~Mathlib.LinearAlgebra.Projection instructions 12.8%
+ ~Mathlib.LinearAlgebra.ProjectiveSpace.Basic instructions -44.3%
- ~Mathlib.LinearAlgebra.Quotient instructions 5.5%
+ ~Mathlib.LinearAlgebra.SModEq instructions -7.5%
+ ~Mathlib.LinearAlgebra.SesquilinearForm instructions -42.2%
+ ~Mathlib.LinearAlgebra.Span instructions -32.7%
+ ~Mathlib.LinearAlgebra.TensorProductBasis instructions -21.8%
+ ~Mathlib.NumberTheory.Basic instructions -38.6%
- ~Mathlib.RingTheory.Adjoin.Fg instructions 11.0%
+ ~Mathlib.RingTheory.EisensteinCriterion instructions -26.6%
+ ~Mathlib.RingTheory.FiniteType instructions -36.3%
+ ~Mathlib.RingTheory.Finiteness instructions -6.4%
+ ~Mathlib.RingTheory.FreeRing instructions -6.3%
+ ~Mathlib.RingTheory.Ideal.QuotientOperations instructions -33.8%
+ ~Mathlib.RingTheory.Localization.Basic instructions -7.1%
+ ~Mathlib.RingTheory.Localization.FractionRing instructions -11.4%
+ ~Mathlib.RingTheory.Localization.Integer instructions -34.9%
+ ~Mathlib.RingTheory.Localization.InvSubmonoid instructions -15.7%
+ ~Mathlib.RingTheory.Localization.Module instructions -11.5%
+ ~Mathlib.RingTheory.Localization.NumDen instructions -12.6%
+ ~Mathlib.RingTheory.Localization.Submodule instructions -12.2%
+ ~Mathlib.RingTheory.MvPolynomial.Basic instructions -13.3%
+ ~Mathlib.RingTheory.Polynomial.Basic instructions -28.9%
+ ~Mathlib.RingTheory.Polynomial.Chebyshev instructions -9.8%
+ ~Mathlib.RingTheory.Polynomial.Eisenstein.Basic instructions -23.4%
+ ~Mathlib.RingTheory.Polynomial.ScaleRoots instructions -26.4%
+ ~Mathlib.RingTheory.PrincipalIdealDomain instructions -16.8%
+ ~Mathlib.RingTheory.QuotientNilpotent instructions -33.4%
+ ~Mathlib.RingTheory.ReesAlgebra instructions -5.8%
+ ~Mathlib.RingTheory.SimpleModule instructions -24.5%
+ ~Mathlib.RingTheory.Subring.Pointwise instructions -11.5%
- ~Mathlib.RingTheory.Valuation.Integers instructions 17.7%
+ ~Mathlib.RingTheory.Valuation.Quotient instructions -25.3%
- ~Mathlib.RingTheory.ZMod instructions 6.2%
+ ~Mathlib.Topology.Algebra.Module.Basic instructions -53.0%
+ ~Mathlib.Topology.Algebra.Module.Determinant instructions -58.0%
+ ~Mathlib.Topology.Algebra.Module.Simple instructions -22.9%
+ ~Mathlib.Topology.Algebra.Module.StrongTopology instructions -71.0%
+ ~Mathlib.Topology.Algebra.Module.WeakDual instructions -26.9%
+ ~Mathlib.Topology.Algebra.Polynomial instructions -38.8%
+ ~Mathlib.Topology.Algebra.StarSubalgebra instructions -5.5%
- ~Mathlib.Topology.Category.Top.Limits.Basic instructions 16.2%
+ ~Mathlib.Topology.Instances.RealVectorSpace instructions -6.5%
- ~Mathlib.Topology.MetricSpace.HausdorffDistance instructions 6.1%
- ~Mathlib.Topology.PathConnected instructions 5.3%
- ~Mathlib.Util.Qq instructions 9.6%
- ~Mathlib.Util.SynthesizeUsing instructions 35.1% |
@@ -320,25 +351,6 @@ end HasDistribNeg | |||
### Rings |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This heading is now a bit stale
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It still looks useful to me: it says that now we are going to talk about properties of rings, while we were dealing with semirings above.
Co-authored-by: Scott Morrison <scott@tqft.net>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM
It's clearly an improvement overall, but it's unfortunate that there are also regressions (in MVPolynomial).
bors d+
Mathlib/Tactic.lean
Outdated
@@ -7,6 +7,7 @@ import Mathlib.Tactic.Backtracking | |||
import Mathlib.Tactic.Basic | |||
import Mathlib.Tactic.ByContra | |||
import Mathlib.Tactic.Cache | |||
import Mathlib.Tactic.CancelDenoms |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Does this PR somehow have a wrong configuration / base branch, given that this line exists?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, I couldn't tell why this line was not picked up by my merge with master, and I had to add it back by hand to make the linter happy. I will merge and see if bors complains.
✌️ sgouezel can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
We make sure that the canonical path from `NonAssocSemiring` to `Ring` passes through `Semiring`, as this is a path which is followed all the time in linear algebra where the defining semilinear map `σ : R →+* S` depends on the `NonAssocSemiring` structure of `R` and `S` while the module definition depends on the `Semiring` structure. Tt is not currently possible to adjust priorities by hand (see lean4#2115). Instead, the last declared instance is used, so we make sure that `Semiring` is declared after `NonAssocRing`, so that `Semiring -> NonAssocSemiring` is tried before `NonAssocRing -> NonAssocSemiring`.
Build failed: |
bors r+ |
We make sure that the canonical path from `NonAssocSemiring` to `Ring` passes through `Semiring`, as this is a path which is followed all the time in linear algebra where the defining semilinear map `σ : R →+* S` depends on the `NonAssocSemiring` structure of `R` and `S` while the module definition depends on the `Semiring` structure. Tt is not currently possible to adjust priorities by hand (see lean4#2115). Instead, the last declared instance is used, so we make sure that `Semiring` is declared after `NonAssocRing`, so that `Semiring -> NonAssocSemiring` is tried before `NonAssocRing -> NonAssocSemiring`.
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
We make sure that the canonical path from `NonAssocSemiring` to `Ring` passes through `Semiring`, as this is a path which is followed all the time in linear algebra where the defining semilinear map `σ : R →+* S` depends on the `NonAssocSemiring` structure of `R` and `S` while the module definition depends on the `Semiring` structure. Tt is not currently possible to adjust priorities by hand (see lean4#2115). Instead, the last declared instance is used, so we make sure that `Semiring` is declared after `NonAssocRing`, so that `Semiring -> NonAssocSemiring` is tried before `NonAssocRing -> NonAssocSemiring`.
We make sure that the canonical path from `NonAssocSemiring` to `Ring` passes through `Semiring`, as this is a path which is followed all the time in linear algebra where the defining semilinear map `σ : R →+* S` depends on the `NonAssocSemiring` structure of `R` and `S` while the module definition depends on the `Semiring` structure. Tt is not currently possible to adjust priorities by hand (see lean4#2115). Instead, the last declared instance is used, so we make sure that `Semiring` is declared after `NonAssocRing`, so that `Semiring -> NonAssocSemiring` is tried before `NonAssocRing -> NonAssocSemiring`.
We make sure that the canonical path from `NonAssocSemiring` to `Ring` passes through `Semiring`, as this is a path which is followed all the time in linear algebra where the defining semilinear map `σ : R →+* S` depends on the `NonAssocSemiring` structure of `R` and `S` while the module definition depends on the `Semiring` structure. Tt is not currently possible to adjust priorities by hand (see lean4#2115). Instead, the last declared instance is used, so we make sure that `Semiring` is declared after `NonAssocRing`, so that `Semiring -> NonAssocSemiring` is tried before `NonAssocRing -> NonAssocSemiring`.
commit 8377ae6b176cc857b383b04173fa5577d09f1689 Author: Matthew Ballard <matt@mrb.email> Date: Wed May 17 21:16:04 2023 -0400 update mathlib.lean commit 8d909eb33ad5e164db2deaf8444b0a21351ec99f Author: Matthew Ballard <matt@mrb.email> Date: Wed May 17 21:14:55 2023 -0400 lint commit 6bcb7f5e70763e15c405912988d867fbe0637691 Author: Matthew Ballard <matt@mrb.email> Date: Wed May 17 21:10:16 2023 -0400 fix last errors commit 1b85bed8887c82368d7da6f4189aea86e98991cb Author: Scott Morrison <scott.morrison@gmail.com> Date: Thu May 18 10:46:42 2023 +1000 fixes commit 519af1d828205304827466024ee65506eb99186e Merge: 98bf9f9b 8bf78812 Author: Scott Morrison <scott.morrison@gmail.com> Date: Thu May 18 09:09:10 2023 +1000 Merge remote-tracking branch 'origin/master' into port/CategoryTheory.Bicategory.Free commit 98bf9f9b293dfe099a631c3bda0bd5e493a7d49e Merge: 1910c612 f9ae3115 Author: Matthew Ballard <matt@mrb.email> Date: Sat May 13 08:31:30 2023 -0400 Merge branch 'master' into port/CategoryTheory.Bicategory.Free commit 1910c612e2e43e3c263f68996ed72b9ac5204f6e Author: Matthew Ballard <matt@mrb.email> Date: Sat May 13 08:31:19 2023 -0400 add new file commit 7af7463b52e7a6d69eb7478235117c023ec8c6aa Merge: f0adc533 269fb63e Author: Matthew Ballard <matt@mrb.email> Date: Sat May 13 08:29:53 2023 -0400 Merge remote-tracking branch 'refs/remotes/origin/port/CategoryTheory.Bicategory.Free' into port/CategoryTheory.Bicategory.Free commit 269fb63e9215d34da56d0b4a7288aca3bde89bc0 Author: Jason Yuen <jason_yuen2007@hotmail.com> Date: Wed May 10 05:02:09 2023 +0000 feat: port Analysis.Normed.Group.ControlledClosure (#3880) commit 628125292856eb71f72eeecd4f5f967f006ec773 Author: Kevin Buzzard <k.buzzard@imperial.ac.uk> Date: Wed May 10 05:02:09 2023 +0000 feat: add some `pp_extended_field_notation`s (#3592) Add some `pp_extended_field_notation`, for opt-in cases with additional arguments. Co-authored-by: Kyle Miller <kmill31415@gmail.com> commit 21708212ef62b7ac824871864a8c3d103f320750 Author: Jason Yuen <jason_yuen2007@hotmail.com> Date: Wed May 10 04:45:22 2023 +0000 feat: port Topology.ContinuousFunction.LocallyConstant (#3877) commit 5d84f9b67af72c588b96bb7821b2523f821b1bec Author: Jason Yuen <jason_yuen2007@hotmail.com> Date: Wed May 10 01:01:27 2023 +0000 feat: port MeasureTheory.Covering.VitaliFamily (#3867) commit 4f3e6145116f5ddf98f9f2615f7e4b129bd02dce Author: Matthew Robert Ballard <matt@mrb.email> Date: Wed May 10 01:01:26 2023 +0000 feat: port Algebra.Category.Group.EquivalenceGroupAddGroup (#3861) commit 0d738a8fef346fb7f9020b327b61fe7f422d1524 Author: Pol_tta <pol_tta@outlook.jp> Date: Wed May 10 01:01:24 2023 +0000 feat: port Dynamics.Ergodic.MeasurePreserving (#3821) Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: MonadMaverick <MonadMaverick@pm.me> commit 9c00193316232966719be6916399504da82103c7 Author: Pol_tta <MonadMaverick@pm.me> Date: Wed May 10 01:01:22 2023 +0000 feat: port MeasureTheory.Measure.OpenPos (#3820) Co-authored-by: Komyyy <pol_tta@outlook.jp> Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com> commit 55413d4565e6e33a8ff7065b20a3f3f9ba18fc0d Author: Jason Yuen <jason_yuen2007@hotmail.com> Date: Wed May 10 00:18:41 2023 +0000 feat: port Analysis.Convex.PartitionOfUnity (#3868) commit 468ee3fa8c1a4a81a0a1ce5829afc0e65226ea97 Author: Pol_tta <pol_tta@outlook.jp> Date: Wed May 10 00:18:39 2023 +0000 feat: port MeasureTheory.Lattice (#3824) Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: MonadMaverick <MonadMaverick@pm.me> commit 01d44eab0e102b78434bd20142f8e1db75e22599 Author: Pol_tta <MonadMaverick@pm.me> Date: Wed May 10 00:18:37 2023 +0000 feat: port MeasureTheory.Measure.MutuallySingular (#3818) Co-authored-by: Komyyy <pol_tta@outlook.jp> Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com> commit 3b3411e0739d9a22e8cabc54b724123a8d773333 Author: Kyle Miller <kmill31415@gmail.com> Date: Wed May 10 00:18:35 2023 +0000 feat: pp_extended_field_notation command to pretty print with dot notation (#3811) The projection notation delaborator that comes from core Lean has some limitations. We introduce a new projection notation delaborator that is able to collapse parent projection sequences, for example `x.toC.toB.toA.val` into `x.val`. The other limitation of the delaborator is that it can only handle true projections that do not have any additional arguments. This commit adds a `pp_extended_field_notation` command to switch on projection notation for specific functions. This command defines app unexpanders that pretty print that function application using dot notation. The app unexpander it produces has a small hack to completely collapse parent projection sequences. Since it is an app unexpander, we do not have access to the actual types, so we use a heuristic that, for example with `A.foo`, if we are looking at `A.foo x.toA y z ...` then we can pretty print this as `x.foo y z`. The projection delaborator is able to collapse parent projection sequences except for the vary last one, so this finishes it off. Note that this heuristic can lead to output that does not round trip if there is a `toA` function that is not a parent projection that happens to be pretty printed with dot notation. commit 7341d34cb0b1173f04f03c7f51daea36a230e35c Author: David Loeffler <d.loeffler.01@cantab.net> Date: Tue May 9 23:59:30 2023 +0000 feat: port Analysis.NormedSpace.CompactOperator (#3805) commit c10b02b9f02a8d212f1ab2cdd18440785e464c58 Author: Scott Morrison <scott@tqft.net> Date: Tue May 9 23:06:55 2023 +0000 feat: port CategoryTheory.Functor.Flat (#3703) Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk> Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> commit 64b7fb14e6a9085f2a3e6fa5bcce317a7120cc3a Author: Pol_tta <MonadMaverick@pm.me> Date: Tue May 9 19:44:35 2023 +0000 feat: port MeasureTheory.Measure.AEMeasurable (#3819) Co-authored-by: Komyyy <pol_tta@outlook.jp> Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com> commit 15da6c20b0e9b06b46b5c6b325f7d21be2d568b7 Author: Jason Yuen <jason_yuen2007@hotmail.com> Date: Tue May 9 10:06:14 2023 +0000 feat: port Probability.ProbabilityMassFunction.Basic (#3865) commit 8ecbd9569ffd605712cd21b65d0d8864520dfb66 Author: Matthew Robert Ballard <matt@mrb.email> Date: Tue May 9 10:06:13 2023 +0000 feat: port CategoryTheory.Preadditive.InjectiveResolution (#3860) Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com> commit da3993ff939d796018ff5e95c41712d1975abfa8 Author: Matthew Robert Ballard <matt@mrb.email> Date: Tue May 9 10:06:12 2023 +0000 feat: port Topology.Category.Top.Limits.Konig (#3853) Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com> commit c3bace0cd04c23c1dd9ab361b03eb80faa8e2c3d Author: Jason Yuen <jason_yuen2007@hotmail.com> Date: Tue May 9 09:46:42 2023 +0000 feat: port MeasureTheory.Measure.Sub (#3866) commit 99bb9fb7ca74cba20b2c2588d2fb9595e5cb98b7 Author: Xavier Roblot <46200072+xroblot@users.noreply.github.com> Date: Tue May 9 08:58:57 2023 +0000 feat port: LinearAlgebra.ProjectiveSpace.Subspace (#3832) commit f273bff58209ed6273afcaf85b7bc554a7ceac3a Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Tue May 9 06:29:09 2023 +0000 chore: tidy various files (#3848) commit cfbec6e28f4c3d117debf58d1338e531cb90a3aa Author: Jason Yuen <jason_yuen2007@hotmail.com> Date: Tue May 9 06:12:54 2023 +0000 feat: port Topology.PartitionOfUnity (#3863) commit 37807d6a99a0199676e029358f20ac5738d9639f Author: Matthew Robert Ballard <matt@mrb.email> Date: Tue May 9 06:12:53 2023 +0000 feat: port CategoryTheory.Preadditive.Injective (#3859) commit b75c4d73f2b15b8234a5dcdca62ad160ae9caf76 Author: Matthew Robert Ballard <matt@mrb.email> Date: Tue May 9 06:12:52 2023 +0000 feat: port Topology.Category.Top.Limits.Cofiltered (#3855) commit b1ee18a7fb8e0079cb0c0fd0fea1afd019219fe5 Author: David Renshaw <dwrenshaw@gmail.com> Date: Tue May 9 06:12:51 2023 +0000 fix: remove unneeded LibrarySearch import (#3854) Removes from `Analysis/SpecificLimits/Normed.lean` an `import Mathlib.Tactic.LibrarySearch` that was accidentally included in #3419. commit 4ddbf238481366ca34965e9d10278833f01a3e70 Author: MonadMaverick <MonadMaverick@pm.me> Date: Tue May 9 05:50:38 2023 +0000 feat: port MeasureTheory.Measure.MeasureSpace (#3324) This PR also renames instances in `MeasureTheory.MeasurableSpace`. Co-authored-by: Komyyy <pol_tta@outlook.jp> Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com> Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com> commit d52008fd7cc8539b1d1b32c9eac2b0aeac276244 Author: Eric Wieser <wieser.eric@gmail.com> Date: Mon May 8 22:44:20 2023 +0000 fix: make `ConcreteCategory.Forget` reducible (#3857) This seems to help in downstream files, [See Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/typeclass.20inference.20not.20seeing.20through.20reducible.20definition/near/356130343) commit a627d110cd7b94a4308c2c71a46f9ed44930bb97 Author: Christopher Hoskin <christopher.hoskin@gmail.com> Date: Mon May 8 21:09:37 2023 +0000 feat: port Topology.ContinuousFunction.Algebra (#3332) Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Christopher Hoskin <christopher.hoskin@overleaf.com> Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Co-authored-by: qawbecrdtey <qawbecrdtey@naver.com> Co-authored-by: Jireh Loreaux <loreaujy@gmail.com> commit 6863ef07ca5aa72edacb87d14977f8816aa3951d Author: sgouezel <sebastien.gouezel@univ-rennes1.fr> Date: Mon May 8 19:26:28 2023 +0000 chore(*): tweak priorities for linear algebra (#3840) We make sure that the canonical path from `NonAssocSemiring` to `Ring` passes through `Semiring`, as this is a path which is followed all the time in linear algebra where the defining semilinear map `σ : R →+* S` depends on the `NonAssocSemiring` structure of `R` and `S` while the module definition depends on the `Semiring` structure. Tt is not currently possible to adjust priorities by hand (see lean4#2115). Instead, the last declared instance is used, so we make sure that `Semiring` is declared after `NonAssocRing`, so that `Semiring -> NonAssocSemiring` is tried before `NonAssocRing -> NonAssocSemiring`. commit a25c78e5c93a3217b9ee46882955746f08469791 Author: Scott Morrison <scott@tqft.net> Date: Mon May 8 13:36:25 2023 +0000 chore: fix name in Mathlib.Topology.Algebra.Module (#3850) Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> commit 51e2e32cd407e1965885af13d1a9bb96e0709c05 Author: Xavier Roblot <46200072+xroblot@users.noreply.github.com> Date: Mon May 8 11:53:12 2023 +0000 feat port: Topology.Algebra.Nonarchimedean.AdicTopology (#3826) commit a5f2b200a2c1fb019a358e347353e19f09402bd5 Author: Jason Yuen <jason_yuen2007@hotmail.com> Date: Mon May 8 11:21:34 2023 +0000 feat: port Data.Complex.Orientation (#3849) commit 2906eb7cfd4f8b36322c63e0209c06e0353a5261 Author: Pol_tta <pol_tta@outlook.jp> Date: Mon May 8 10:01:09 2023 +0000 feat: port MeasureTheory.Tactic (#3816) commit b5c7cda33ead3895a3e92b9b41112bdc755a433a Author: Jujian Zhang <jujian.zhang1998@outlook.com> Date: Mon May 8 09:17:50 2023 +0000 feat: definition of krull dimension for a preordered set (#3704) Given a preordered set $(S, <)$, the krull dimension of $S$ is defined to be $\sup\{n | a_0 < a_1 < ... < a_n\}$ where the supremum takes place in extended natural numbers $\mathbb N \cup \{\pm \infty\}$, i.e. empty set is negative-infinite dimensional and a set with arbitrary long $a_0 < a_1 < ... < a_n$ is positive dimensional. Similar constructions in mathlib does require a chain to be nonempty so that empty set would have the wrong dimension, so I defined a new structure `StrictSeries` to avoid confusion with `chain`; in this structure, the underlying list is always nonempty. commit 8685958b7012efbeb848057bc4b936aaa4c39b63 Author: Pol_tta <pol_tta@outlook.jp> Date: Mon May 8 05:55:43 2023 +0000 fix: remove lambda abstraction of `Nat.rec_zero` and `Nat.rec_add_one` (#3839) ```lean theorem rec_zero {C : ℕ → Sort u} (h0 : C 0) (h : ∀ n, C n → C (n + 1)) : (Nat.rec h0 h : ∀ n, C n) 0 = h0 := rfl ``` The above theorem is elaborated as follow: ```lean theorem rec_zero {C : ℕ → Sort u} (h0 : C 0) (h : ∀ n, C n → C (n + 1)) : (fun n => Nat.rec h0 h n) 0 = h0 := rfl ``` This form of the theorem isn't generic. This PR fixes this problem. Co-authored-by: Pol_tta <52843868+Komyyy@users.noreply.github.com> commit b840606e7074798762c81e73e53ac4ab2e661de5 Author: Xavier Roblot <46200072+xroblot@users.noreply.github.com> Date: Mon May 8 05:55:41 2023 +0000 feat port: LinearAlgebra.Orientation (#3777) I had to add a bunch of `set_option synthInstance.etaExperiment true`, `set_option maxHeartbeats` and `set_option synthInstance.maxHeartbeats` to this file I tried to use the methods described in this [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/maxHeartbeats/near/356217898) to remove some of the `maxHeartbeats` but I was not successful. Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> commit 882005842a71af115186357b21dd4f2bbfe2a597 Author: Jason Yuen <jason_yuen2007@hotmail.com> Date: Mon May 8 05:55:40 2023 +0000 feat: port Analysis.SpecificLimits.Normed (#3419) Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> commit c2cf5ba958fb0ac9b1536f66d98b73a486aabaee Author: Pol_tta <pol_tta@outlook.jp> Date: Mon May 8 03:29:54 2023 +0000 fix: `lift` can't be used when the type of the goal is `Sort.{?u}` while `?u` is assigned by `0` (#3800) For example, this emits error. ```lean example (n : ℕ) : n = 0 ∨ ∃ p : ℕ+, n = p := by by_cases hn : 0 < n · lift n to ℕ+ using hn -- error right exact ⟨n, rfl⟩ · left exact Nat.eq_zero_of_nonpos _ hn ``` The cause is that `lift` doesn't instantiate level metavariables when checking that the type of the goal is `Prop`. This PR makes the above example available. Please refer to `test/lift.lean`. commit 3dd4e55886338c90af2571a024a0418d4fe6b09a Author: Yury G. Kudryashov <urkud@urkud.name> Date: Mon May 8 03:29:53 2023 +0000 feat: port Data.Sym.Card (#3109) Co-authored-by: int-y1 <jason_yuen2007@hotmail.com> commit 016b02ed781f7804fe6c002d33eabc205a5e30de Author: Pol_tta <pol_tta@outlook.jp> Date: Mon May 8 03:07:17 2023 +0000 feat: port Computability.Partrec (#3830) commit 28e49fca3bcedc90c9149a26c10c338ebc00d7a5 Author: Jason Yuen <jason_yuen2007@hotmail.com> Date: Mon May 8 02:51:12 2023 +0000 feat: port Topology.Category.Top.OpenNhds (#3834) commit a5a10ca18c91a12454b6317e637d69586c33448c Author: Eric Wieser <wieser.eric@gmail.com> Date: Mon May 8 00:54:18 2023 +0000 chore: forward-port leanprover-community/mathlib#18878 (#3742) commit 4350c4e364eda158598503baf5916729406f4e95 Author: Yury G. Kudryashov <urkud@urkud.name> Date: Mon May 8 00:54:17 2023 +0000 feat: port Analysis.Normed.Group.Quotient (#3457) Co-authored-by: Mauricio Collares <mauricio@collares.org> commit cd0670b6fbe9fc3398ce064cd55f7464e15d7353 Author: Moritz Doll <moritz.doll@googlemail.com> Date: Mon May 8 00:35:14 2023 +0000 chore: add explicit name for instances in Analysis.Seminorm (#3759) Some names were extremely long. Example: [Seminorm.instConditionallyCompleteLatticeSeminormToSeminormedRingToSeminormedCommRingToNormedCommRingToAddGroupToSMulToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToSMulZeroClassToZeroToCommMonoidWithZeroToCommGroupWithZeroToSemifieldToFieldToSMulWithZeroToMonoidWithZeroToSemiringToDivisionSemiringToMulActionWithZeroToAddCommMonoid](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Seminorm.html#Seminorm.instConditionallyCompleteLatticeSeminormToSeminormedRingToSeminormedCommRingToNormedCommRingToAddGroupToSMulToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToSMulZeroClassToZeroToCommMonoidWithZeroToCommGroupWithZeroToSemifieldToFieldToSMulWithZeroToMonoidWithZeroToSemiringToDivisionSemiringToMulActionWithZeroToAddCommMonoid) commit 6045f2042e5e14e3b45a9ca56bf2be04921827dd Author: Moritz Firsching <moritz.firsching@gmail.com> Date: Sun May 7 14:02:40 2023 +0000 feat: port Algebra.ContinuedFractions.Computation.Translations (#3794) Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> commit 0285c2bf3919356b608125ae878487201d15b488 Author: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Date: Sun May 7 13:25:52 2023 +0000 chore: forward port leanprover-community/mathlib#18951 (#3837) commit 0633b89bb4e7148fcb22a6c26915d79838a11ad5 Author: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Date: Sun May 7 09:18:13 2023 +0000 chore: forward port leanprover-community/mathlib#18866 (#3813) commit b3b1b7dd2388506eceadab75d83ca8183aeeb496 Author: Scott Morrison <scott@tqft.net> Date: Sun May 7 09:18:12 2023 +0000 feat: library_search tries most specific lemmas first, and then those with shorter names first (#3725) It turns out that `DiscrTree.getMatch` returns more specific results later than less specific ones, and so we want to put a `.reverse` in, as `library_search` is more likely to be able to make use of the more specific lemmas. Additionally, within each "batch" of lemmas in the DiscrTree, we sort them so that those with shorter names are tried before those with longer names. You shouldn't expect this to be anymore successful, I think, but maybe the user will be happier getting shorter results rather than longer ones. See some further discussion at [zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/library_search.20timeout/near/356406350). - [x] depends on: #3771 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> commit c993a4e8f1a1d2c587b3d939af778d3bf3dff420 Author: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Date: Sun May 7 08:52:06 2023 +0000 chore: forward port leanprover-community/mathlib#18479 (#3829) commit 038caab459760a87b476351dfd62b7ab2a50bee5 Author: Scott Morrison <scott@tqft.net> Date: Sun May 7 08:35:59 2023 +0000 feat: speedup library_search by using two DiscrTrees (#3771) Previously, `library_search` used a single `DiscrTree`. There is a cached `DiscrTree` covering the whole library (and which is cached to disk), and then when we call `library_search`, we traverse the declarations in the current file, adding those into that `DiscrTree`. This PR speeds up that process by using a second independent `DiscrTree` for the declarations in the current file. This means that the cached tree for the library does not need to be "edited in place", and so we save some time. On the test file on my computer this speeds up from around 10.0s to around 8.2s. When calling `library_search` low down in a large file we should expect larger gains. The PR also does some refactoring work on `DeclCache`, which will be useful if/when we install global caching for other lookup tactics such as `propose` or [`rewrites`](https://github.com/leanprover-community/mathlib4/pull/3119). Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> commit 18c6e24d4a7c5ec87e4c7e9e295e852475c70c55 Author: Eric Wieser <wieser.eric@gmail.com> Date: Sun May 7 07:13:52 2023 +0000 chore: forward-port leanprover-community/mathlib#18934 (#3806) Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> commit 424263023c2e9c1588f05d9a28a5abb9ae8ae88b Author: Eric Wieser <wieser.eric@gmail.com> Date: Sun May 7 07:13:51 2023 +0000 chore: forward-port leanprover-community/mathlib#18902 (#3770) commit 8a2c2bf047940fdad965814424f3a2c1d8a6644d Author: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Date: Sun May 7 05:02:30 2023 +0000 chore: bye-bye, solo `by`s! (#3825) This PR puts, with one exception, every single remaining `by` that lies all by itself on its own line to the previous line, thus matching the current behaviour of `start-port.sh`. The exception is when the `by` begins the second or later argument to a tuple or anonymous constructor; see https://github.com/leanprover-community/mathlib4/pull/3825#discussion_r1186702599. Essentially this is `s/\n *by$/ by/g`, but with manual editing to satisfy the linter's max-100-char-line requirement. The Python style linter is also modified to catch these "isolated `by`s". commit 2d3d9fe6f82530f0355cf06d52cfa44bfbb1a033 Author: Hagb (Junyu Guo 郭俊余) <hagb@hagb.name> Date: Sat May 6 19:50:27 2023 +0000 feat(Data/MvPolynomial/Basic): add and generalize some lemmas from Finsupp and MonoidAlgebra (#3604) Most of these changes generalize from `DistribMulAction` to `SmulZeroClass`. The new lemmas are all just proved using corresponding lemmas on the underlying types. Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com> commit 55705f9084276a7a7de523230af1827ba60fb949 Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Sat May 6 19:21:52 2023 +0000 ci: make bors block on the check_imported job (#3827) commit f72485cdca5b6010514168873616232d7765dc90 Author: Scott Morrison <scott@tqft.net> Date: Sat May 6 15:10:58 2023 +0000 chore: bump to Lean 4 nightly-2023-05-06 (#3817) Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> commit f1ae5b7ec8d705042684482b8fb06cd34adfcb65 Author: Scott Morrison <scott@tqft.net> Date: Sat May 6 12:10:21 2023 +0000 feat: enable cancel_denoms preprocessor in linarith (#3801) Enable the `cancelDenoms` preprocessor in `linarith`. Closes #2714. - [x] depends on: #3797 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Patrick Massot <patrickmassot@free.fr> Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> commit ec38b915d3a36cb7d0adef661259453be01c4728 Author: MonadMaverick <pol_tta@outlook.jp> Date: Sat May 6 11:29:51 2023 +0000 feat: port MeasureTheory.Measure.NullMeasurable (#3349) Co-authored-by: MonadMaverick <MonadMaverick@pm.me> Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com> commit d8f1f02fd6a548ea4d1f944972a929089cca5869 Author: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Date: Sat May 6 08:46:32 2023 +0000 chore: forward port leanprover-community/mathlib#18910 (#3814) commit 79ca50dced9a0a479fd0da6941f7cd67a9927d9e Author: Patrick Massot <patrickmassot@free.fr> Date: Sat May 6 08:46:30 2023 +0000 feat: `cancel_denoms` tactic (#3797) Ports the tactic `CancelDenoms.derive` and the interactive tactic `cancel_denoms`. This tactic is needed to make `linarith` handle divisions by numbers, but this PR does not involve `linarith`. Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com> commit b7ed6f5bb61ecc043f01aa3b27276188ba1a2cdf Author: Yury G. Kudryashov <urkud@urkud.name> Date: Sat May 6 08:29:50 2023 +0000 chore: fix names (#3812) Forward-port leanprover-community/mathlib#18921 and leanprover-community/mathlib#18924 commit 0fbb715e696b40a5dfa8974c9f59a890a65fd2b7 Author: Xavier Roblot <46200072+xroblot@users.noreply.github.com> Date: Sat May 6 07:33:35 2023 +0000 feat port : RingTheory.Ideal.AssociatedPrime (#3810) commit a31acfcf3520728bef79bcfa4e0275466a0834ab Author: EmilieUthaiwat <emiliepathum@gmail.com> Date: Sat May 6 07:17:10 2023 +0000 feat: port LinearAlgebra.Lagrange (#3784) commit 2617ac0e6b300c20d8bb10198fafe9332d45df5a Author: MonadMaverick <MonadMaverick@pm.me> Date: Sat May 6 06:40:03 2023 +0000 feat: port MeasureTheory.Measure.AEDisjoint (#3351) Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Co-authored-by: Komyyy <pol_tta@outlook.jp> commit 214014d2c39d5fe770fbb305588808bcb1a4aff4 Author: Scott Morrison <scott@tqft.net> Date: Fri May 5 22:16:38 2023 +0000 chore: forward-port backports (#3752) * `data.mv_polynomial.basic`, `data.mv_polynomial.funext`: leanprover-community/mathlib#18839 * `category_theory.limits.preserves.finite`, `category_theory.preadditive.projective`: leanprover-community/mathlib#18890 * `category_theory.abelian.basic`, `category_theory.abelian.opposite`: leanprover-community/mathlib#18740 * `topology.category.Top.limits.basic`: leanprover-community/mathlib#18871. Note that this does not show a useful diff on the dashboard pages as file splits aren't tracked well by git. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> commit 35f51927282d120df99e96c037ddfb4132e947bf Author: Eric Wieser <yael.dillies@gmail.com> Date: Fri May 5 14:00:33 2023 +0000 chore: forward-port leanprover-community/mathlib#18906 (#3798) commit ddf1a04c942b901a07d053d2f967f2ad40777e1a Author: Jason Yuen <jason_yuen2007@hotmail.com> Date: Fri May 5 13:44:48 2023 +0000 feat: port MeasureTheory.Function.AEMeasurableSequence (#3803) commit e0fd3f7dbf994599af312d5f630bf7fcedbb9bce Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Fri May 5 12:24:18 2023 +0000 chore: tidy various files (#3718) commit f4dd3adaf6847e2e940853c1d3d2b36aaa781425 Author: Eric Wieser <wieser.eric@gmail.com> Date: Fri May 5 06:25:34 2023 +0000 chore: update SHA from #3753 (#3799) I forgot to update it in #3753. commit 963ac8132f80aa069680b719e64cb4b0cba54366 Author: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Date: Thu May 4 19:07:27 2023 +0000 feat: port Algebra.ContinuedFractions.ConvergentsEquiv (#3795) commit 3a802fc9446bc158d1486997f5f5794e4c402beb Author: Yaël Dillies <yael.dillies@gmail.com> Date: Thu May 4 16:30:32 2023 +0000 feat: well-founded or transitive relations don't have cycles (#3793) Match https://github.com/leanprover-community/mathlib/pull/18512 Co-authored-by: Eric Wieser <wieser.eric@gmail.com> commit d9ea05decd47313168b7f7febd64643ff7ed1932 Author: Eric Wieser <wieser.eric@gmail.com> Date: Thu May 4 11:23:11 2023 +0000 chore: forward-port leanprover-community/mathlib#18922 (#3779) commit 4b452a9fec289cc8ed1e18098680ab0db19079d4 Author: Eric Wieser <wieser.eric@gmail.com> Date: Thu May 4 11:23:10 2023 +0000 chore: forward-port leanprover-community/mathlib#18876 (#3753) commit 45acfec0369c6720452249bdf860cbeafa89c25b Author: Eric Wieser <wieser.eric@gmail.com> Date: Thu May 4 11:23:09 2023 +0000 chore: forward-port leanprover-community/mathlib#18879 (#3741) commit 700eb94e185cb781b1f8945cb350ff3051f4a52a Author: Moritz Firsching <moritz.firsching@gmail.com> Date: Thu May 4 09:12:04 2023 +0000 feat: port Algebra.ContinuedFractions.TerminatedStable (#3792) Co-authored-by: Moritz Firsching <firsching@google.com> commit d7a6de21586b9f2fd41676da624f6fc4ccd3eb18 Author: Jason Yuen <jason_yuen2007@hotmail.com> Date: Thu May 4 09:12:03 2023 +0000 feat: port Algebra.ContinuedFractions.Computation.Basic (#3788) Co-authored-by: Moritz Firsching <firsching@google.com> commit c643d1282c5c47f210c9497d1e19867dbd1bcb74 Author: MonadMaverick <MonadMaverick@pm.me> Date: Thu May 4 08:44:21 2023 +0000 feat: port MeasureTheory.Measure.MeasureSpaceDef (#3325) Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Co-authored-by: Komyyy <pol_tta@outlook.jp> commit 6ee07bd7ff39032233031f056c2649ccda4cafef Author: Moritz Firsching <moritz.firsching@gmail.com> Date: Thu May 4 08:21:57 2023 +0000 feat: port Algebra.ContinuedFractions.ContinuantsRecurrence (#3791) Co-authored-by: Moritz Firsching <firsching@google.com> commit ac2e5438c8c07b7c63166df1bdf15076028c4159 Author: Moritz Firsching <moritz.firsching@gmail.com> Date: Thu May 4 05:47:35 2023 +0000 feat: port Algebra.ContinuedFractions.Translations (#3783) Co-authored-by: Moritz Firsching <firsching@google.com> commit e34f9b0fc494772fc304aeffa32e829278a17962 Author: Kyle Miller <kmill31415@gmail.com> Date: Wed May 3 23:01:50 2023 +0000 feat: delaborators for Finset.prod and Finset.sum (#3772) Also fixes some spacing in their `syntax` commands, which impacts pretty printing. commit d490330ae628c357fe9c758990605ded66628194 Author: Kevin Buzzard <k.buzzard@imperial.ac.uk> Date: Wed May 3 22:31:52 2023 +0000 chore: update Mathlib/Tactic.lean (#3727) Co-authored-by: Scott Morrison <scott.morrison@gmail.com> commit 2f62a68be3bd7b099d591820492b5eb668f3843e Author: Alex J Best <alex.j.best@gmail.com> Date: Wed May 3 17:20:53 2023 +0000 feat: implement intermediate state for simp_rw (#3738) closes #3680, see https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Stepping.20through.20simp_rw/near/326712986 commit ee67ae82322f25cafc7534b5dbd33ad93d8faa8b Author: thorimur <68410468+thorimur@users.noreply.github.com> Date: Wed May 3 14:00:58 2023 +0000 refactor, fix: `MetaM` version of `rfl` tactic and missing `whnfR`/`instantiateMVars` (#3758) This PR factors out a `MetaM` version of the `rfl` tactic and adds a missing `whnfR` and `instantiateMVars` in front of the goal type. This means that a few `rw`s across mathlib4 now close the goal instead of e.g. requiring a trailing `exact le_rfl`. Note: we do not use `whnfR` on the return type when adding the `refl` extension in the first place, as `forallMetaTelescopeReducing` already performs `whnf` (here, at reducible transparency). See [zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.233758.20.E2.80.93.20rfl.20refactor.20.26.20fix) for some discussion on the internal changes made. Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com> commit 8cad0a826486d2a0005de7e353e12f2ae143b78e Author: Jason Yuen <jason_yuen2007@hotmail.com> Date: Wed May 3 13:39:19 2023 +0000 feat: port LinearAlgebra.AffineSpace.FiniteDimensional (#3670) commit 052deed907b6ffc756bd7ce4ecdedf4d6db1068d Author: JeEyben <124388640+JeEyben@users.noreply.github.com> Date: Wed May 3 13:39:17 2023 +0000 feat: port RingTheory.Localization.InvSubmonoid (#3384) Co-authored-by: int-y1 <jason_yuen2007@hotmail.com> commit 5a77592a11f98444a19c2ea97fad0291fe408b96 Author: Jason Yuen <jason_yuen2007@hotmail.com> Date: Wed May 3 13:39:15 2023 +0000 feat: port Algebra.ContinuedFractions.Basic (#3379) Co-authored-by: Jon Eugster <eugster.jon@gmail.com> commit 8f6e4d2054a99fd8c847cacfe57b408b8b18646a Author: Moritz Firsching <moritz.firsching@gmail.com> Date: Wed May 3 13:39:13 2023 +0000 feat: port CategoryTheory.Monoidal.Free.Basic (#2808) Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr> Co-authored-by: Johan Commelin <johan@commelin.net> commit 30a890eb4e9dbda9dd9dc42c4e2f260b59abb214 Author: Scott Morrison <scott@tqft.net> Date: Wed May 3 13:16:44 2023 +0000 fix: a missing TypeMax (#3781) One was missed; curiously it wasn't harmful in `master`, but when we turn on `etaExperiment` globally this causes a breakage Co-authored-by: Scott Morrison <scott.morrison@gmail.com> commit 814f492f80e97836913d1b788911a1ddc76b6f42 Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Wed May 3 12:09:25 2023 +0000 chore: move shortcut instance to Algebra.Algebra.Basic (#3778) See https://github.com/leanprover-community/mathlib/pull/18907 Co-authored-by: Eric Wieser <wieser.eric@gmail.com> commit 0ab5e61ca44a52206df99830a0facaf91d8b803e Author: Moritz Doll <moritz.doll@googlemail.com> Date: Wed May 3 11:33:41 2023 +0000 docs: fix names in Analysis.LocallyConvex.Bounded (#3774) commit ac0fd896f1bb1f197f25f5f654a859b4a02d8516 Author: MonadMaverick <MonadMaverick@pm.me> Date: Wed May 3 11:02:26 2023 +0000 feat: port MeasureTheory.Measure.OuterMeasure (#3674) Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Komyyy <pol_tta@outlook.jp> Co-authored-by: Johan Commelin <johan@commelin.net> commit ae90d57d66ab4137eb22d9152cdd2d6aa0f19cd6 Author: Jason Yuen <jason_yuen2007@hotmail.com> Date: Wed May 3 06:27:24 2023 +0000 feat: port LinearAlgebra.AffineSpace.Matrix (#3775) commit 3ad45ada879ff7d1eb0c425df6bf8d4bec66adba Author: Xavier-François Roblot <46200072+xroblot@users.noreply.github.com> Date: Wed May 3 01:24:20 2023 +0000 feat port: Algebra.FreeModule.Determinant (#3767) commit c577bee1ea0537d6a4488ad569f3252ed2123784 Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Wed May 3 01:24:19 2023 +0000 feat: port Data.Complex.Determinant (#3765) commit c89277f05e074a327f79381c14d659b05e68168b Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Wed May 3 01:24:17 2023 +0000 feat: port Analysis.SpecialFunctions.Trigonometric.Chebyshev (#3764) commit 1dac593b7e1c149c4d234973754b4347de968595 Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Wed May 3 01:24:16 2023 +0000 feat: port Analysis.Convex.Complex (#3763) commit efb20cbedfb68cb1b2967449ef92b374c0f9724b Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Wed May 3 01:24:16 2023 +0000 feat: port Data.Matrix.Rank (#3762) commit a65601d186c742e05cece1797b1046322f8f16f4 Author: Joël Riou <joel.riou@universite-paris-saclay.fr> Date: Wed May 3 01:24:14 2023 +0000 feat: port CategoryTheory.Category.Groupoid (#3761) commit 4ddf8c7c266db2c9486475955bfb75a6ccafc360 Author: Yaël Dillies <yael.dillies@gmail.com> Date: Wed May 3 01:24:13 2023 +0000 chore: tweak `subsingleton_of_trichotomous_of_irrefl` (#3749) Match https://github.com/leanprover-community/mathlib/pull/18749 commit 94cd04e32c71f1a64c15e6aee06eabaa6c059fb4 Author: Scott Morrison <scott@tqft.net> Date: Tue May 2 22:58:39 2023 +0000 feat: better display of partial results from library_search (#3743) On @PatrickMassot's [example](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/library_search.20regression/near/353375130): ```lean import Mathlib.Topology.Instances.Real import Mathlib.Topology.Algebra.Order.Compact import Mathlib.Tactic.LibrarySearch example (f : ℝ → ℝ) {K : Set ℝ} (hK: IsCompact K) : ∃ x ∈ K, ∀ y ∈ K, f x ≤ f y := by library_search ``` we have: * `refine IsCompact.exists_forall_le hK ?_ ?_` as one of the suggested solutions * in fact, as the first solution (on the basis that it uses more local hypotheses than alternatives) * none of the spurious results which use `False.elim ?_` * and better display of the result, with hints: ```lean refine IsCompact.exists_forall_le hK ?_ ?_ -- Remaining subgoals: -- ⊢ Set.Nonempty K -- ⊢ ContinuousOn (fun x ↦ f x) K ``` Co-authored-by: Scott Morrison <scott.morrison@gmail.com> commit 391cddce21029cb45a255a2ab063c7d3b98b4b60 Author: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Date: Tue May 2 16:51:37 2023 +0000 feat: port Topology.Algebra.Module.Determinant (#3766) commit fed5a971cac804f30a3b4b2550bc532e0b1adbaf Author: Scott Morrison <scott@tqft.net> Date: Tue May 2 14:49:42 2023 +0000 fix: don't look too hard for binders when indexing lemmas for library_search (#3724) Co-authored-by: Scott Morrison <scott.morrison@gmail.com> commit 3f6f6282cc137af13d6c480744e58dedca712c1e Author: Scott Morrison <scott@tqft.net> Date: Tue May 2 12:23:16 2023 +0000 fix: linarith variable shadowing bug (#3760) As reported on [zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/linarith.20bug). Co-authored-by: Scott Morrison <scott.morrison@gmail.com> commit 92a23d50515de9ac1baf29a66826ee77305b2b91 Author: Joël Riou <joel.riou@universite-paris-saclay.fr> Date: Tue May 2 10:23:03 2023 +0000 feat: port CategoryTheory.Monoidal.Tor (#3754) Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com> commit 179b81ee4cadef2f601e1f1265d266ea0cf91cd7 Author: Eric Wieser <wieser.eric@gmail.com> Date: Tue May 2 10:23:02 2023 +0000 Revert "feat: port Algebra.Order.ToIntervalMod (#2148)" (#3388) This reverts commit 2d0dd3902a4a796d8f38778fec991ab1d4c2a660. The porting comments say "Would be nice to finish leanprover-community/mathlib#17743 first". The commit message says "Might be best to wait". We should wait; there is no urgency to merge this, and no discussion took place that argued against waiting. commit 3f6b46f277537242649fa82a62efddb09fc8dfea Author: Pol_tta <reddeloostw@gmail.com> Date: Tue May 2 10:05:14 2023 +0000 feat: port LinearAlgebra.Determinant (#3694) Co-authored-by: int-y1 <jason_yuen2007@hotmail.com> Co-authored-by: Komyyy <pol_tta@outlook.jp> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> commit 8d401bd92990dec5d9d1aa59094789f607caf2d0 Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Tue May 2 07:59:21 2023 +0000 feat: port Data.Complex.Module (#3737) Co-authored-by: int-y1 <jason_yuen2007@hotmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> commit 0227fbbc71c1ce40bb9338c52058d0a34565653c Author: Alex J Best <alex.j.best@gmail.com> Date: Mon May 1 22:19:23 2023 +0000 chore: update workflows to avoid deprecation (#3755) Forward port of https://github.com/leanprover-community/mathlib/pull/18761 - https://github.com/leanprover-community/mathlib/pull/18765 but a bit simpler as we dont have as many things set up yet. commit 6d40a326339dc6b42c3ed25a607bb5bfe035bc7f Author: Joël Riou <joel.riou@universite-paris-saclay.fr> Date: Mon May 1 22:19:22 2023 +0000 feat: port CategoryTheory.Functor.LeftDerived (#3751) Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> commit e57a8f962faca1a6949a74daec03e5b350995af8 Author: Joël Riou <joel.riou@universite-paris-saclay.fr> Date: Mon May 1 22:19:21 2023 +0000 feat: port CategoryTheory.Sites.LeftExact (#3706) commit fc3894f2f75c7b860783e8a90fd767bcb00b2cb9 Author: Pol_tta <pol_tta@outlook.jp> Date: Mon May 1 22:19:20 2023 +0000 feat: make `Acc.rec` and many related defs computable (#3535) Lean 4 code generator has had no native supports for `Acc.rec`. This PR makes `Acc.rec` computable. This change makes many defs computable. Especially, computable `PFun.fix` and `Part.hasFix` enables us to reason about `partial` functions. This PR also renames some instances and gives `PFun.lift` `@[coe]` attr. commit eb1f66662c488bafde47edd140eef4a47bc59d2a Author: Bulhwi Cha <chabulhwi@semmalgil.com> Date: Mon May 1 22:02:09 2023 +0000 refactor: delete `import` line (#3745) Delete an unnecessary `import` line. commit 28ae9843458339c54de11f62fce84002528759af Author: Joël Riou <joel.riou@universite-paris-saclay.fr> Date: Mon May 1 20:06:10 2023 +0000 feat: port CategoryTheory.Preadditive.ProjectiveResolution (#3740) Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com> commit 52e6ad71693190465481e0ae20d97913dbba06e9 Author: Yaël Dillies <yael.dillies@gmail.com> Date: Mon May 1 17:47:55 2023 +0000 chore: Move lattice `finset` lemmas around (#3748) Match https://github.com/leanprover-community/mathlib/pull/18900 Co-authored-by: Eric Wieser <wieser.eric@gmail.com> commit 5b940a6dc1a1bd5f2f4a6f271059bbea0e3857bc Author: Yury G. Kudryashov <urkud@urkud.name> Date: Mon May 1 17:47:54 2023 +0000 feat: port CategoryTheory.Abelian.Exact (#3638) Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr> commit 0ea443f63e211696d5a166c82f7469cc2cdc1d82 Author: Yaël Dillies <yael.dillies@gmail.com> Date: Mon May 1 15:10:19 2023 +0000 feat: `f.update i '' Icc a b = Icc (f.update i a) (f.update i b)` (#3747) Match https://github.com/leanprover-community/mathlib/pull/18892 * [`order.lattice`@`d6aad9528ddcac270ed35c6f7b5f1d8af25341d6`..`e4bc74cbaf429d706cb9140902f7ca6c431e75a4`](https://leanprover-community.github.io/mathlib-port-status/file/order/lattice?range=d6aad9528ddcac270ed35c6f7b5f1d8af25341d6..e4bc74cbaf429d706cb9140902f7ca6c431e75a4) * [`algebra.group.pi`@`90df25ded755a2cf9651ea850d1abe429b1e4eb1`..`e4bc74cbaf429d706cb9140902f7ca6c431e75a4`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/pi?range=90df25ded755a2cf9651ea850d1abe429b1e4eb1..e4bc74cbaf429d706cb9140902f7ca6c431e75a4) * [`data.set.intervals.pi`@`4020ddee5b4580a409bfda7d2f42726ce86ae674`..`e4bc74cbaf429d706cb9140902f7ca6c431e75a4`](https://leanprover-community.github.io/mathlib-port-status/file/data/set/intervals/pi?range=4020ddee5b4580a409bfda7d2f42726ce86ae674..e4bc74cbaf429d706cb9140902f7ca6c431e75a4) Co-authored-by: Eric Wieser <wieser.eric@gmail.com> commit e95cccde5645c855b0c08a5fb4d944adf442a4b7 Author: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Date: Mon May 1 13:19:51 2023 +0000 feat: port Topology.Category.Profinite.Projective (#3746) commit 55637dc9d43c30243cb0d8578cabcabf4dedbc8c Author: Moritz Firsching <moritz.firsching@gmail.com> Date: Mon May 1 11:02:54 2023 +0000 feat: port Mathlib.Data.Ordmap.Ordnode (#1455) Co-authored-by: Arien Malec <arien.malec@gmail.com> Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com> Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: qawbecrdtey <qawbecrdtey@kaist.ac.kr> commit 64d186af31d440f3743d6862c0f39cf553fcdca1 Author: Violeta Hernández <vi.hdz.p@gmail.com> Date: Mon May 1 08:43:35 2023 +0000 feat: port ZFC set intersection (#3345) Also fixes some erroneous theorem names from the port. [`set_theory.zfc.basic`@`98bbc3526516bca903bff09ea10c4206bf079e6b`..`f0b3759a8ef0bd8239ecdaa5e1089add5feebe1a`](https://leanprover-community.github.io/mathlib-port-status/file/set_theory/zfc/basic?range=98bbc3526516bca903bff09ea10c4206bf079e6b..f0b3759a8ef0bd8239ecdaa5e1089add5feebe1a) Mathlib 3: https://github.com/leanprover-community/mathlib/pull/18232 Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> commit 5925a364a984ab06f0d1b425339c4bb5cd1b2646 Author: Scott Morrison <scott@tqft.net> Date: Mon May 1 01:58:20 2023 +0000 feat: port Topology.Category.Profinite.Basic (#3705) Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: adamtopaz <github@adamtopaz.com> commit c272f4940037d117009ce720b7aba0bad3986627 Author: Alex J Best <alex.j.best@gmail.com> Date: Mon May 1 01:36:18 2023 +0000 feat: annotate build errors in the github files changed tab using an action (#3739) This is suboptimal as it doesn't handle multiline comments, but it is better than nothing, and the implementation works out of the box. This is broadly similar to the support we had in mathlib 3, but the implementation is different as we no longer have json errors as an option, so must instead match an errorformat directly (the gcc one works fine). Supporting multiline error messages appears not to be possible using the builtin output without further processing with the current state of problem matchers supported by github (which follow the vscode design). Thus to get an improvement on this the build output must be piped through a second program that processes it in some way, or a lake build type command should be added that outputs in a required format. Likewise to get annotations for linter failures we will need to add extra information to the linter output, either setting the annotations ourselves (as we did in mathlib 3) or at least adding line numbers to the existing output so that we can at least match it with a problem matcher again. commit 77416707240d45fb64906bc8f7f28d6f29cfda2b Author: Bulhwi Cha <chabulhwi@semmalgil.com> Date: Sun Apr 30 23:31:19 2023 +0000 chore: move theorems on `String` to std4 (#3712) https://github.com/leanprover/std4/pull/124 moves the following from Mathlib4 to Std4: * helper `simp` theorems on `String.Pos` * `String.utf8GetAux.inductionOn` commit 6a64ec0b0f5ee12b611215ac7ad1e0145465a327 Author: Ruben Van de Velde <reddeloostw@gmail.com> Date: Sun Apr 30 11:38:03 2023 +0000 feat: port FieldTheory.Tower (#3716) Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> commit 76707255936de099ae6835e7ddbe5f7bf95a7a36 Author: Joël Riou <joel.riou@universite-paris-saclay.fr> Date: Sat Apr 29 23:07:53 2023 +0000 feat: port Algebra.Category.Group.ZModuleEquivalence (#3732) commit 543b8ec1ea21d7a3321234bb0b6532576a897c61 Author: Joël Riou <joel.riou@universite-paris-saclay.fr> Date: Sat Apr 29 23:07:52 2023 +0000 feat: port AlgebraicTopology.ExtraDegeneracy (#3729) commit eb11681ef13f0d1aba2ff267a20bd08883484f82 Author: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Date: Sat Apr 29 22:52:42 2023 +0000 feat: port CategoryTheory.Monad.Coequalizer (#3733) commit 6a28eee3a21942016a01bbada70ce9a6a40ba8e5 Author: Moritz Firsching <moritz.firsching@gmail.com> Date: Sat Apr 29 22:28:56 2023 +0000 chore: no newline before aligns (#3735) Co-authored-by: Moritz Firsching <firsching@google.com> commit a7e9e4ab120a3b6d10251d3c3d24a1e60c13dca8 Author: Yaël Dillies <yael.dillies@gmail.com> Date: Sat Apr 29 16:26:38 2023 +0000 feat: `a * b ≠ b ↔ a ≠ 1` (#3726) https://github.com/leanprover-community/mathlib/pull/18635 * [`algebra.group.basic`@`2196ab363eb097c008d4497125e0dde23fb36db2`..`84771a9f5f0bd5e5d6218811556508ddf476dcbd`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/basic?range=2196ab363eb097c008d4497125e0dde23fb36db2..84771a9f5f0bd5e5d6218811556508ddf476dcbd) * [`algebra.order.field.basic`@`44e29dbcff83ba7114a464d592b8c3743987c1e5`..`84771a9f5f0bd5e5d6218811556508ddf476dcbd`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/order/field/basic?range=44e29dbcff83ba7114a464d592b8c3743987c1e5..84771a9f5f0bd5e5d6218811556508ddf476dcbd) Co-authored-by: Eric Wieser <wieser.eric@gmail.com> commit dc012f816b787bcb80007f2bc1b5e6604aa57b28 Author: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Date: Sat Apr 29 13:32:59 2023 +0000 feat: port LinearAlgebra.ProjectiveSpace.Independence (#3728) Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com> commit 8dd639e1083340aed6138d8ad7f954091b037267 Author: Scott Morrison <scott@tqft.net> Date: Sat Apr 29 13:32:58 2023 +0000 fix: find MathlibExtras from downstream projects (#3721) Co-authored-by: Scott Morrison <scott.morrison@gmail.com> commit 73bab6a59163675f3f1f26530bac9c2571eba84b Author: Scott Morrison <scott@tqft.net> Date: Sat Apr 29 13:32:57 2023 +0000 fix: allow library_search to run when maxHeartbeats = 0 (#3720) Co-authored-by: Scott Morrison <scott.morrison@gmail.com> commit 301ea2db46c56d28eb73f418ab992b0010e5f75d Author: Yaël Dillies <yael.dillies@gmail.com> Date: Sat Apr 29 13:32:56 2023 +0000 chore: Remove `finset.sup_finset_image` (#3713) Match https://github.com/leanprover-community/mathlib/pull/18893 Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com> commit f667fdec730173011b40f4dcea8c79c33eed39b6 Author: Joël Riou <joel.riou@universite-paris-saclay.fr> Date: Sat Apr 29 13:32:55 2023 +0000 feat: port CategoryTheory.Abelian.Transfer (#3424) commit 029b212612c336f75d26163cebd5e129a455847e Author: Alex J Best <alex.j.best@gmail.com> Date: Sat Apr 29 10:38:07 2023 +0000 feat: allow several tactics on types that are slightly less obviously Types (#3682) Many tactics attempt to get the universe of the sort of the terms involved by matching on the level being a succ of something. Unfortunately this fails on some nontrivial examples like mvpolynomial which can have type `Sort (max (u+1) (v+1))` Instead we decrement the level manually after matching it. See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60ring.60.20tactic.20cannot.20prove.20equality.20about.20.60MvPolynomial.60/near/352549549 This PR modifies ring, ring_nf, nontriviality, polyrith, linarith, and some norm_num handlers to appropriately handle this. Test cases showing examples that failed before (inspired by the case of mvpolynomial, but in principle there could be other interesting types that have multiple universe parameters in this way, some of which may even have a linear order who knows). In doing so we factor out `inferTypeQ'` into its own file `Mathlib.Tactic.Qq` for mathlib-relevant extensions of Qq commit a540fe1433f247fd5cd6561401ab813cf04a5e9e Author: Yury G. Kudryashov <urkud@urkud.name> Date: Sat Apr 29 09:57:49 2023 +0000 feat: port LinearAlgebra.ProjectiveSpace.Basic (#3692) commit d2c96a57df11efb8eec9f31377e5de800012433c Author: Jason Yuen <jason_yuen2007@hotmail.com> Date: Sat Apr 29 05:39:03 2023 +0000 chore: add hash for Data.MvPolynomial.Polynomial (#3723) commit 288a7d79cf1b6dfd4940082700efa5b8dc15d496 Author: Jason Yuen <jason_yuen2007@hotmail.com> Date: Sat Apr 29 03:33:44 2023 +0000 feat: port LinearAlgebra.SymplecticGroup (#3696) commit 3230cdeee0ab5da8fc47680e4d5da87addcc90e7 Author: Alex J Best <alex.j.best@gmail.com> Date: Fri Apr 28 23:45:34 2023 +0000 feat: make alias compile code when possible (#3719) commit 36844e9cb778e4e857c8c9b0b0339c876679f4a8 Author: Eric Wieser <wieser.eric@gmail.com> Date: Fri Apr 28 23:45:32 2023 +0000 chore: forward-port leanprover-community/mathlib#18880 (#3717) commit 24f74e319f706f55aef284703cddec753ffadb62 Author: Yaël Dillies <yael.dillies@gmail.com> Date: Fri Apr 28 23:19:17 2023 +0000 chore: Rename to `AddLocalization` (#3714) This name wasn't properly capitalised. commit aaf828ddcf36204db88d6e02fa5a90da2126a1bb Author: Eric Wieser <wieser.eric@gmail.com> Date: Fri Apr 28 21:59:08 2023 +0000 chore: update SHA (#3711) I forgot to update the SHA in #3675 commit b50e5c5aa89de2b79df485083b3f5c1bb00b4b8d Author: Yury G. Kudryashov <urkud@urkud.name> Date: Fri Apr 28 21:59:07 2023 +0000 feat: port LinearAlgebra.Matrix.Diagonal (#3695) Some proofs in the last section were failing even with eta-experiment, so I generalized some lemmas from `Field`s to `Semifield`s. commit f5f2fbf04d6c9b0a995807c408ade9e71bad05f1 Author: Adam Topaz <github@adamtopaz.com> Date: Fri Apr 28 18:56:37 2023 +0000 feat: Port Topology.Category.CompHaus.Projective (#3715) commit 863aebc8ccf10ff0c19a25fad7344e8a585c9108 Author: Xavier-François Roblot <46200072+xroblot@users.noreply.github.com> Date: Fri Apr 28 17:46:02 2023 +0000 feat LinearAlgebra.Basis: add basis.restrictScalars (#3707) Mathlib4 version of https://github.com/leanprover-community/mathlib/pull/18814 [`linear_algebra.basis`@`2f4cdce0c2f2f3b8cd58f05d556d03b468e1eb2e`..`04cdee31e196e30f507e8e9eb2d06e02c9ff6310`](https://leanprover-community.github.io/mathlib-port-status/file/linear_algebra/basis?range=2f4cdce0c2f2f3b8cd58f05d556d03b468e1eb2e..04cdee31e196e30f507e8e9eb2d06e02c9ff6310)) commit a585b6ffc2dc1351ab8a5aa1534c26f22c2d7910 Author: Yaël Dillies <yael.dillies@gmail.com> Date: Fri Apr 28 14:30:45 2023 +0000 feat: Lemmas relating definitions of infinite sets (#3672) Match https://github.com/leanprover-community/mathlib/pull/18620 * [`data.set.finite`@`c941bb9426d62e266612b6d99e6c9fc93e7a1d07`..`52fa514ec337dd970d71d8de8d0fd68b455a1e54`](https://leanprover-community.github.io/mathlib-port-status/file/data/set/finite?range=c941bb9426d62e266612b6d99e6c9fc93e7a1d07..52fa514ec337dd970d71d8de8d0fd68b455a1e54) * [`data.finset.locally_finite`@`f24cc2891c0e328f0ee8c57387103aa462c44b5e`..`52fa514ec337dd970d71d8de8d0fd68b455a1e54`](https://leanprover-community.github.io/mathlib-port-status/file/data/finset/locally_finite?range=f24cc2891c0e328f0ee8c57387103aa462c44b5e..52fa514ec337dd970d71d8de8d0fd68b455a1e54) * [`data.nat.lattice`@`2445c98ae4b87eabebdde552593519b9b6dc350c`..`52fa514ec337dd970d71d8de8d0fd68b455a1e54`](https://leanprover-community.github.io/mathlib-port-status/file/data/nat/lattice?range=2445c98ae4b87eabebdde552593519b9b6dc350c..52fa514ec337dd970d71d8de8d0fd68b455a1e54) commit 601c82017f39b855b6a697a78d4a244b668996e7 Author: Moritz Firsching <moritz.firsching@gmail.com> Date: Fri Apr 28 14:00:44 2023 +0000 feat: port LinearAlgebra.Matrix.Transvection (#3700) Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com> commit 3d576486048be2cbae503d1c1e7f5a0a85b66a6c Author: Yaël Dillies <yael.dillies@gmail.com> Date: Fri Apr 28 11:44:00 2023 +0000 feat: For any `b`, there exists a set `s` of independent atoms such that `Sup s` is the complement of `b` (#3588) Match https://github.com/leanprover-community/mathlib/pull/8475 * [`order.compactly_generated`@`210657c4ea4a4a7b234392f70a3a2a83346dfa90`..`e8cf0cfec5fcab9baf46dc17d30c5e22048468be`](https://leanprover-community.github.io/mathlib-port-status/file/order/compactly_generated?range=210657c4ea4a4a7b234392f70a3a2a83346dfa90..e8cf0cfec5fcab9baf46dc17d30c5e22048468be) * [`order.directed`@`485b24ed47b1b7978d38a1e445158c6224c3f42c`..`e8cf0cfec5fcab9baf46dc17d30c5e22048468be`](https://leanprover-community.github.io/mathlib-port-status/file/order/directed?range=485b24ed47b1b7978d38a1e445158c6224c3f42c..e8cf0cfec5fcab9baf46dc17d30c5e22048468be) commit d3e6edfe83effc9316d710b3e4421b16162e73d1 Author: Joël Riou <joel.riou@universite-paris-saclay.fr> Date: Fri Apr 28 11:10:45 2023 +0000 feat: port CategoryTheory.Action (#3657) commit bc85faaf38cdda2b9c3f808ba563c232f5f815a0 Author: Yury G. Kudryashov <urkud@urkud.name> Date: Fri Apr 28 11:10:44 2023 +0000 feat: port CategoryTheory.Preadditive.Projective (#3615) Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> commit b98b04707b0c77941e61f598a4b8c8164a2c2482 Author: Moritz Firsching <moritz.firsching@gmail.com> Date: Fri Apr 28 10:54:06 2023 +0000 feat: port LinearAlgebra.Matrix.ZPow (#3671) Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> commit cd980733e0e92568cb77dbb4a9c0f6b3498dc9ce Author: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Date: Fri Apr 28 09:49:14 2023 +0000 feat: port LinearAlgebra.Matrix.FiniteDimensional (#3698) commit 740bbec09993a7a71a993aaf7fdee3571005215c Author: Bulhwi Cha <chabulhwi@semmalgil.com> Date: Fri Apr 28 09:32:10 2023 +0000 refactor: change arguments order (#3701) Change the order of the arguments to `String.utf8GetAux.add_right_cancel`. commit 4d1c8e0454e1470c3cbc8e3aa41d5745acd1cdc1 Author: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Date: Fri Apr 28 06:56:28 2023 +0000 feat: port LinearAlgebra.Matrix.InvariantBasisNumber (#3697) commit 15d98e6b55a610e11d16e02aca4fc7be760c5ffd Author: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Date: Fri Apr 28 06:56:27 2023 +0000 feat: port AlgebraicTopology.Nerve (#3693) commit e35da366b8e442a61e77516edd8197e8715264b5 Author: Eric Wieser <wieser.eric@gmail.com> Date: Fri Apr 28 06:56:26 2023 +0000 forward-port leanprover-community/mathlib#18840 (#3678) commit d456dd3ce4146aa82e05ac02aae437901b534fc1 Author: Eric Wieser <wieser.eric@gmail.com> Date: Fri Apr 28 06:56:25 2023 +0000 chore: forward-port leanprover-community/mathlib#18802 (#3677) commit e234e1dbab60d5cb2491ee19f608fe6357d7244c Author: Eric Wieser <wieser.eric@gmail.com> Date: Fri Apr 28 06:56:24 2023 +0000 chore: forward-port leanprover-community/mathlib#18869 (#3676) commit bd1736fa511c00b8607b3e1134213cd963b923c1 Author: Eric Wieser <wieser.eric@gmail.com> Date: Fri Apr 28 06:56:23 2023 +0000 chore: forward-port leanprover-community/mathlib#18842 (#3675) commit 7d4f125478272f478180c413365372d3069e8a63 Author: Yaël Dillies <yael.dillies@gmail.com> Date: Fri Apr 28 06:56:22 2023 +0000 feat: The equivalence between `fin n → fin m` and `fin (m ^ n)` (#3673) Match https://github.com/leanprover-community/mathlib/pull/14817 [`algebra.big_operators.fin`@`f93c11933efbc3c2f0299e47b8ff83e9b539cbf6`..`cdb01be3c499930fd29be05dce960f4d8d201c54`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/big_operators/fin?range=f93c11933efbc3c2f0299e47b8ff83e9b539cbf6..cdb01be3c499930fd29be05dce960f4d8d201c54) Co-authored-by: Eric Wieser <wieser.eric@gmail.com> commit 535bb666094594a96afc3f425fe1c5cd49261836 Author: Eric Wieser <wieser.eric@gmail.com> Date: Fri Apr 28 06:56:21 2023 +0000 chore: forward-port leanprover-community/mathlib#18833 (#3660) The previously hacky proofs with porting notes can be discarded in favor of the ones from mathport. commit 7f09ac6a714e33333682d4f6ff7c95bac10684d2 Author: Floris van Doorn <fpvdoorn@gmail.com> Date: Fri Apr 28 06:56:19 2023 +0000 perf: improve performance of `to_additive` (#3632) * `applyReplacementFun` now treats applications `f x_1 ... x_n` as atomic, and recurses directly into `f` and `x_i` (before it recursed on the partial appliations `f x_1 ... x_j`) * I had to reimplement the way `to_additive` reorders arguments, so at the same time I also made it more flexible. We can now reorder with an arbitrary permutation, and you have to specify this by providing a permutation using cycle notation (e.g. `(reorder := 1 2 3, 8 9)` means we're permuting the first three arguments and swapping arguments 8 and 9). This implements the first item of #1074. * `additiveTest` now memorizes the test on previously-visited subexpressions. Thanks to @kmill for this suggestion! The performance on (one of) the slowest declaration(s) to additivize (`MonoidLocalization.lift`) is summarized below (note: `dsimp only` refers to adding a single `dsimp only` tactic in the declaration, which was done in #3580) ``` original: 27400ms better applyReplacementFun: 1550ms better applyReplacementFun + better additiveTest: 176ms dsimp only: 6710ms better applyReplacementFun + dsimp only: 425ms better applyReplacementFun + better additiveTest + dsimp only: 128ms ``` commit ccfc417d5df188a52936f4722ab1162a22b9e162 Author: Pol_tta <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Fri Apr 28 05:58:44 2023 +0000 feat: port LinearAlgebra.Matrix.Basis (#3691) Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Komyyy <pol_tta@outlook.jp> Co-authored-by: Johan Commelin <johan@commelin.net> commit 6fc9d5e9d711f3812bbd7cd0fbeb2fed11cf9c6e Author: Jeremy Tan Jie Rui <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Fri Apr 28 05:41:51 2023 +0000 feat: port LinearAlgebra.FreeModule.Finite.Matrix (#3690) Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net> commit 7b0b99d0366fcca78f849aaef42e8dcd0975ed66 Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Fri Apr 28 03:54:51 2023 +0000 feat: port LinearAlgebra.Matrix.ToLin (#3552) Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> commit 4f6380966f207897ef1487010c80d15f24769971 Author: Joël Riou <joel.riou@universite-paris-saclay.fr> Date: Fri Apr 28 02:53:49 2023 +0000 feat: port AlgebraicTopology.SimplicialSet (#3689) commit 7b88b65bd51282f240fc40b1bd6c1e7d8c227be6 Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Fri Apr 28 02:53:48 2023 +0000 ci: lint references.bib (#3683) Ported from mathlib3. commit b8ad9541c1a9fb132cad12283b3accc56c5ed35e Author: Moritz Firsching <moritz.firsching@gmail.com> Date: Fri Apr 28 02:53:47 2023 +0000 chore: rename Zpowers -> ZPowers (#3681) Co-authored-by: Moritz Firsching <firsching@google.com> commit eb417549e64541742039abd0dc9b823388124907 Author: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Date: Fri Apr 28 02:33:14 2023 +0000 feat: port Topology.Algebra.Module.Multilinear (#3348) Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: ADedecker <anatolededecker@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> commit fe28ed480a44857c878f429eabc66b9fee4f3a45 Author: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Date: Fri Apr 28 01:23:38 2023 +0000 feat: port Topology.Algebra.Module.StrongTopology (#3684) Co-authored-by: ADedecker <anatolededecker@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> commit 1113f1cefa6387fb404087427f48596810d95acb Author: Henrik Böving <hargonix@gmail.com> Date: Fri Apr 28 00:11:16 2023 +0000 fix: mathlib4_docs cleanup routine (#3631) commit ed822e7be3f58018b6fd816b957fd888db4b35c2 Author: Kevin Buzzard <k.buzzard@imperial.ac.uk> Date: Thu Apr 27 23:33:25 2023 +0000 feat : port CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit (#3605) This was harder than it looked (the proofs are long and broke). Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Scott Morrison <scott@tqft.net> commit 78d77dfbcae2747913005e50dad80692cb1ff940 Author: Adam Topaz <github@adamtopaz.com> Date: Thu Apr 27 23:18:23 2023 +0000 feat: Port Topology.Category.CompHaus.Basic (#3688) Relatively straightforward port. Co-authored-by: Scott Morrison <scott@tqft.net> commit d1a1c6b104967ffed8ca69ebb4f3ea9a4eb25424 Author: Joël Riou <joel.riou@universite-paris-saclay.fr> Date: Thu Apr 27 21:43:33 2023 +0000 feat: port Analysis.Convex.StoneSeparation (#3686) commit 2f36c58966790d0a91aaa910836751e289259f12 Author: Joël Riou <joel.riou@universite-paris-saclay.fr> Date: Thu Apr 27 21:43:32 2023 +0000 feat: port CategoryTheory.Noetherian (#3685) commit aaa5e0a421c8b53d60e6b7d1341ade2d5b2e59b3 Author: Felix-Weilacher <fweilach@andrew.cmu.edu> Date: Thu Apr 27 21:26:10 2023 +0000 chore: forward port leanprover-community/mathlib#18864 (#3687) Forward port changes from leanprover-community/mathlib#18864 to Topology/Perfect.lean and MeasureTheory/MeasurableSpace.lean Co-authored-by: Eric Wieser <wieser.eric@gmail.com> commit 2dab08df0323c6e58ace9b611c7e951602d0a2c0 Author: Joël Riou <joel.riou@universite-paris-saclay.fr> Date: Thu Apr 27 15:27:17 2023 +0000 feat: port CategoryTheory.Sites.Adjunction (#3663) commit c934e5d186bdc16bb6f0b181e3ebe1e95acbe333 Author: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com> Date: Thu Apr 27 14:06:46 2023 +0000 chore: forward-port generalisation (#3679) * [`data.finsupp.basic`@`2651125b48fc5c170ab1111afd0817c903b1fc6c`..`57911c5a05a1b040598e1e1…
We make sure that the canonical path from
NonAssocSemiring
toRing
passes throughSemiring
,as this is a path which is followed all the time in linear algebra where the defining semilinear map
σ : R →+* S
depends on theNonAssocSemiring
structure ofR
andS
while the moduledefinition depends on the
Semiring
structure.Tt is not currently possible to adjust priorities by hand (see lean4#2115). Instead, the last
declared instance is used, so we make sure that
Semiring
is declared afterNonAssocRing
, sothat
Semiring -> NonAssocSemiring
is tried beforeNonAssocRing -> NonAssocSemiring
.I have tried other options to streamline things, with less success. This change is both the least disruptive and the best I have found.