Skip to content

Conversation

astrainfinita
Copy link
Collaborator

@astrainfinita astrainfinita commented Oct 30, 2024

CommRing.toRing is an exception. CommRing is so important that it needs to be looked up early. An important goal of #7873 is also to search for Zero/One/Add/Mul instances first along Zero/One/Add/Mul -> ... -> Ring -> CommRing -> Field.


From #7873.

Open in Gitpod

Copy link

github-actions bot commented Oct 30, 2024

PR summary 51ade5646b

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas 1543 1336 -207 (-13.42%)
Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity 1552 1352 -200 (-12.89%)
Mathlib.NumberTheory.NumberField.Discriminant.Defs 1646 1441 -205 (-12.45%)
Mathlib.NumberTheory.Padics.PadicNumbers 1290 1142 -148 (-11.47%)
Mathlib.Topology.MetricSpace.Polish 1268 1259 -9 (-0.71%)
Import changes for all files
Files Import difference
Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas -207
Mathlib.NumberTheory.NumberField.Discriminant.Defs -205
Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity Mathlib.NumberTheory.SumTwoSquares -200
Mathlib.NumberTheory.Padics.PadicNumbers Mathlib.NumberTheory.Harmonic.Int -148
Mathlib.NumberTheory.Padics.PadicIntegers -109
Mathlib.Algebra.Homology.Embedding.Basic -101
Mathlib.NumberTheory.Padics.RingHoms -89
Mathlib.RingTheory.WittVector.Compare -84
Mathlib.Algebra.Module.LinearMap.Rat Mathlib.Algebra.Module.Rat -37
12 files Mathlib.Algebra.Star.Module Mathlib.CategoryTheory.Monoidal.Linear Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic Mathlib.Algebra.Algebra.Unitization Mathlib.CategoryTheory.Quotient.Linear Mathlib.Algebra.Homology.ShortComplex.Linear Mathlib.RepresentationTheory.Action.Limits Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed Mathlib.CategoryTheory.Monoidal.Subcategory Mathlib.Algebra.Homology.Linear Mathlib.CategoryTheory.Linear.LinearFunctor
-33
4 files Mathlib.Algebra.Homology.Embedding.HomEquiv Mathlib.Algebra.Homology.Embedding.Extend Mathlib.Algebra.Homology.Embedding.Boundary Mathlib.Algebra.Homology.Embedding.Restriction
-29
21 files Mathlib.Data.Matrix.Auto Mathlib.Data.Matrix.Invertible Mathlib.Data.Matrix.Composition Mathlib.Data.Matrix.Basic Mathlib.Data.Matrix.Basis Mathlib.GroupTheory.Coxeter.Matrix Mathlib.Data.Matrix.PEquiv Mathlib.Data.Matrix.CharP Mathlib.Data.Matrix.Block Mathlib.CategoryTheory.Preadditive.Mat Mathlib.Data.Matrix.Reflection Mathlib.LinearAlgebra.Matrix.Trace Mathlib.LinearAlgebra.Matrix.Symmetric Mathlib.Data.Matrix.RowCol Mathlib.Data.Matrix.DualNumber Mathlib.Data.Matrix.Hadamard Mathlib.Combinatorics.Optimization.ValuedCSP Mathlib.Combinatorics.SimpleGraph.IncMatrix Mathlib.Data.Matrix.Notation Mathlib.LinearAlgebra.Matrix.Circulant Mathlib.LinearAlgebra.Matrix.Orthogonal
-25
10 files Mathlib.LinearAlgebra.FinsuppVectorSpace Mathlib.Algebra.Category.ModuleCat.Adjunctions Mathlib.LinearAlgebra.Matrix.Ideal Mathlib.LinearAlgebra.Matrix.DotProduct Mathlib.Algebra.Module.Projective Mathlib.RepresentationTheory.Action.Monoidal Mathlib.LinearAlgebra.TensorProduct.Basis Mathlib.RingTheory.Localization.FractionRing Mathlib.LinearAlgebra.FreeModule.Basic Mathlib.LinearAlgebra.StdBasis
-10
Mathlib.Topology.MetricSpace.Polish Mathlib.Topology.MetricSpace.Perfect -9
Mathlib.GroupTheory.Coxeter.Basic -8
3 files Mathlib.Data.Rat.Denumerable Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal Mathlib.MeasureTheory.Constructions.Polish.Basic
-5

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

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

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

@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 30, 2024
@mathlib4-dependent-issues-bot
Copy link
Collaborator

mathlib4-dependent-issues-bot commented Oct 30, 2024

@astrainfinita astrainfinita changed the base branch from master to FR_18472_base November 5, 2024 03:48
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 6, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 6, 2024
@astrainfinita
Copy link
Collaborator Author

!bench

@leanprover-bot

This comment was marked as outdated.

This comment was marked as outdated.

@YaelDillies YaelDillies deleted the branch FR_18472_base August 15, 2025 16:36
@YaelDillies YaelDillies deleted the FR_comm_lower branch August 15, 2025 16:38
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
awaiting-bench blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) slow-typeclass-synthesis t-algebra Algebra (groups, rings, fields, etc)
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants