Skip to content

chore: adjust Module.Finite instance priority#37522

Open
matthewjasper wants to merge 1 commit intoleanprover-community:masterfrom
matthewjasper:finite-module-priority
Open

chore: adjust Module.Finite instance priority#37522
matthewjasper wants to merge 1 commit intoleanprover-community:masterfrom
matthewjasper:finite-module-priority

Conversation

@matthewjasper
Copy link
Copy Markdown
Collaborator

@matthewjasper matthewjasper commented Apr 1, 2026

Make instances that are rarely going to be helpful lower priority.
Increase the priority of FiniteDimensional.complexToReal, because it's more likely correct than the other priority 100 Module.Finite instances.

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Apr 1, 2026

PR summary 4609a29824

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ instance (priority := 100) (R S : Type*) [CommSemiring R] [StrongRankCondition R] [Semiring S]
+ instance (priority := 500) FiniteDimensional.complexToReal (E : Type*) [AddCommGroup E]
+ instance (priority := 90) instFiniteDimensionalOfIsReflexive (K V : Type*)
- instFiniteDimensionalOfIsReflexive
- instance (R S : Type*) [CommSemiring R] [StrongRankCondition R] [Semiring S] [Algebra R S]
- instance (priority := 100) FiniteDimensional.complexToReal (E : Type*) [AddCommGroup E]

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.

No changes to technical debt.

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).

@github-actions github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Apr 1, 2026
@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Apr 2, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Apr 2, 2026 •
edited
Loading

Benchmark results for c8ba0ba against 4609a29 are in. There are no significant changes. @grunweg

  • ✅ build//instructions: -27.0G (-0.02%)

Small changes (11✅)

  • ✅ build/module/Mathlib.Algebra.Lie.Derivation.Killing//instructions: -427.2M (-2.50%)
  • ✅ build/module/Mathlib.Algebra.Lie.TraceForm//instructions: -4.6G (-4.00%)
  • ✅ build/module/Mathlib.AlgebraicGeometry.Artinian//instructions: -1.5G (-9.61%)
  • ✅ build/module/Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite//instructions: -1.7G (-3.26%)
  • ✅ build/module/Mathlib.Analysis.Matrix.Spectrum//instructions: -887.4M (-1.95%)
  • ✅ build/module/Mathlib.FieldTheory.Finite.GaloisField//instructions: -668.1M (-2.50%)
  • ✅ build/module/Mathlib.FieldTheory.Finite.Trace//instructions: -436.5M (-4.73%)
  • ✅ build/module/Mathlib.FieldTheory.Galois.NormalBasis//instructions: -483.2M (-1.69%)
  • ✅ build/module/Mathlib.FieldTheory.Relrank//instructions: -3.0G (-2.85%)
  • ✅ build/module/Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis//instructions: -1.8G (-3.89%)
  • ✅ build/module/Mathlib.NumberTheory.NumberField.CMField//instructions: -1.8G (-1.77%)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@matthewjasper @grunweg @leanprover-radar