Skip to content

[Merged by Bors] - feat(RingTheory): IsStandardEtale#32138

Closed
erdOne wants to merge 4 commits intoleanprover-community:masterfrom
erdOne:erd1/isStandardEtale
Closed

[Merged by Bors] - feat(RingTheory): IsStandardEtale#32138
erdOne wants to merge 4 commits intoleanprover-community:masterfrom
erdOne:erd1/isStandardEtale

Conversation

@erdOne
Copy link
Copy Markdown
Member

@erdOne erdOne commented Nov 26, 2025


Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 26, 2025

PR summary 1159dce834

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.RingTheory.Etale.StandardEtale 1462 1478 +16 (+1.09%)
M scripts/count-trans-deps.py
M scripts/count-trans-deps.py
M scripts/count-trans-deps.py
Import changes for all files
Files Import difference
Mathlib.RingTheory.Etale.StandardEtale 16

Declarations diff

+ IsStandardEtale
+ IsStandardEtale.of_equiv
+ IsStandardEtale.of_isLocalizationAway
+ IsStandardEtale.of_surjective
+ StandardEtalePresentation
+ StandardEtalePresentation.aeval_val_equivMvPolynomial
+ StandardEtalePresentation.equivRing
+ StandardEtalePresentation.equivRing_symm_X
+ StandardEtalePresentation.equivRing_x
+ StandardEtalePresentation.exists_mul_aeval_x_g_pow_eq_aeval_x
+ StandardEtalePresentation.mapEquiv
+ StandardEtalePresentation.toPresentation
+ StandardEtalePresentation.toSubmersivePresentation
+ StandardEtalePresentation.toSubmersivePresentation_jacobian
+ iff_of_surjective
+ instance (P : StandardEtalePair R) : IsStandardEtale R P.Ring
+ instance (priority := low) [IsStandardEtale R S] : Algebra.Etale R S
+ instance : Algebra.Etale R P.Ring
+ instance : IsStandardEtale R R
+ ker_ofAlgHom
+ of_restrictScalars
+ pderiv_one_equivMvPolynomial
+ pderiv_zero_equivMvPolynomial
- Algebra.FormallyEtale.iff_of_surjective
- Algebra.FormallyEtale.of_restrictScalars
- Polynomial.Bivariate.pderiv_one_equivMvPolynomial
- Polynomial.Bivariate.pderiv_zero_equivMvPolynomial

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.


No changes to technical debt.

You can run this locally as

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

@erdOne erdOne requested a review from chrisflav November 26, 2025 12:58
@chrisflav chrisflav added t-ring-theory Ring theory awaiting-author A reviewer has asked the author a question or requested changes. labels Nov 26, 2025
@erdOne erdOne removed the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 26, 2025
@chrisflav
Copy link
Copy Markdown
Member

Thanks!

maintainer merge

@github-actions
Copy link
Copy Markdown

🚀 Pull request has been placed on the maintainer queue by chrisflav.

@ghost ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Nov 27, 2025
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Nov 27, 2025
mathlib-bors bot pushed a commit that referenced this pull request Nov 27, 2025
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 27, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(RingTheory): IsStandardEtale [Merged by Bors] - feat(RingTheory): IsStandardEtale Nov 27, 2025
@mathlib-bors mathlib-bors bot closed this Nov 27, 2025
mathlib-bors bot pushed a commit that referenced this pull request Dec 11, 2025
@YaelDillies YaelDillies deleted the erd1/isStandardEtale branch April 3, 2026 15:09
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR has been sent to bors. t-ring-theory Ring theory

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants