Skip to content

test make HasQuotient out put a setoid#15586

Draft
astrainfinita wants to merge 7 commits intomasterfrom
FR_test_quotient_setoid
Draft

test make HasQuotient out put a setoid#15586
astrainfinita wants to merge 7 commits intomasterfrom
FR_test_quotient_setoid

Conversation

@astrainfinita
Copy link
Copy Markdown
Collaborator

@astrainfinita astrainfinita commented Aug 7, 2024

Open in Gitpod

@astrainfinita astrainfinita added the t-algebra Algebra (groups, rings, fields, etc) label Aug 7, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 7, 2024 •
edited
Loading

PR summary 39c99fe2aa

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ instHasQuotient
+ instance : HasQuotient M (LieSubmodule R L M) (fun m ↦ m.toSubmodule.quotientRel) := ⟨⟩
- instance : HasQuotient M (LieSubmodule R L M)

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.

@astrainfinita astrainfinita mentioned this pull request Aug 7, 2024
Open
1 task
@astrainfinita
Copy link
Copy Markdown
Collaborator Author

astrainfinita commented Aug 9, 2024

!bench

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Aug 9, 2024

Here are the benchmark results for commit 72c0e89.
There were significant changes against commit faf7c20:

  Benchmark                                        Metric         Change
  ======================================================================
- ~Mathlib.Algebra.Module.PID                      instructions    11.3%
- ~Mathlib.AlgebraicGeometry.EllipticCurve.Group   instructions     8.0%
- ~Mathlib.LinearAlgebra.Semisimple                instructions    16.8%
- ~Mathlib.NumberTheory.KummerDedekind             instructions    27.9%
- ~Mathlib.NumberTheory.RamificationInertia        instructions    16.2%
- ~Mathlib.RingTheory.AdjoinRoot                   instructions    58.0%
- ~Mathlib.RingTheory.Ideal.Quotient               instructions    38.0%
- ~Mathlib.RingTheory.Ideal.QuotientOperations     instructions   115.1%
- ~Mathlib.RingTheory.Jacobson                     instructions    24.7%
- ~Mathlib.RingTheory.Kaehler.Basic                instructions    18.2%
- ~Mathlib.RingTheory.Polynomial.Quotient          instructions    43.9%

@astrainfinita
Copy link
Copy Markdown
Collaborator Author

astrainfinita commented Aug 9, 2024

!bench

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Aug 9, 2024

Here are the benchmark results for commit 39c99fe.
There were significant changes against commit faf7c20:

  Benchmark                                      Metric         Change
  ====================================================================
- ~Mathlib.NumberTheory.RamificationInertia      instructions     9.5%
- ~Mathlib.RingTheory.AdjoinRoot                 instructions    19.4%
- ~Mathlib.RingTheory.Ideal.QuotientOperations   instructions    27.8%
- ~Mathlib.RingTheory.Kaehler.Basic              instructions     6.3%

@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 17, 2024
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

merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@astrainfinita @leanprover-bot