[Merged by Bors] - chore(RingTheory/{Algebraic, Localization/Integral}): rename decls to use dot notation #8437
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…larger_base_of_injective
adomani
force-pushed
the
adomani/reduce_IsIntegral_dot
branch
from
099c72b
to
2ea97ec
Compare
adomani
force-pushed
the
adomani/reduce_IsIntegral_dot
branch
from
2ea97ec
to
6280639
Compare
adomani
added
the
awaiting-review
renameDecl -i isAlgebraic_of_finite IsAlgebraic.of_finite renameDecl -i isAlgebraic_of_larger_base IsAlgebraic.of_larger_base renameDecl -i isIntegral_add IsIntegral.add renameDecl -i isIntegral_map_of_comp_eq_of_isIntegral IsIntegral.map_of_comp_eq renameDecl -i isIntegral_mul IsIntegral.mul renameDecl -i isIntegral_neg IsIntegral.neg renameDecl -i isIntegral_ofSubring IsIntegral.of_subring renameDecl -i isIntegral_of_finite IsIntegral.of_finite renameDecl -i isIntegral_of_isIntegral_mul_unit IsIntegral.of_mul_unit renameDecl -i isIntegral_of_mem_closure IsIntegral.of_mem_closure renameDecl -i isIntegral_of_mem_of_FG IsIntegral.of_mem_of_fg renameDecl -i isIntegral_of_pow IsIntegral.of_pow renameDecl -i isIntegral_smul IsIntegral.smul renameDecl -i isIntegral_sub IsIntegral.sub renameDecl -i isIntegral_tower_bot_of_isIntegral IsIntegral.tower_bot renameDecl -i isIntegral_tower_bot_of_isIntegral_field IsIntegral.tower_bot_of_field renameDecl -i map_isIntegral IsIntegral.map renameDecl -i mem_integralClosure_iff_mem_FG mem_integralClosure_iff_mem_fg
eric-wieser
reviewed
Nov 16, 2023
| @@ -136,23 +136,23 @@ theorem isAlgebraic_of_mem_rootSet {R : Type u} {A : Type v} [Field R] [Field A] | |||
|
|
|||
| open IsScalarTower | |||
|
|
|||
| theorem isAlgebraic_algebraMap_of_isAlgebraic {a : S} : | |||
| protected theorem IsAlgebraic.algebraMap {a : S} : | |||
There was a problem hiding this comment.
I assume the protected was not handled by the tool?
There was a problem hiding this comment.
Correct, although there is the possibility of flagging declarations that you want to protect in a future version of the renaming tool: the ilean files that I use contains where the declaration is defined.
There was a problem hiding this comment.
However, more basic features are missing in the tool, so I haven't given much thought to this.
eric-wieser
approved these changes
Nov 16, 2023
|
✌️ adomani can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-mathlib4-bot
added
delegated
and removed
awaiting-review
|
Though perhaps we should address @jcommelin's comment first:
|
jcommelin
changed the title
|
I think the list of renames should go into the pr description. |
|
Done |
|
@jcommelin, my personal opinion is that using |
|
Resolved privately bors merge Thanks! |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Nov 16, 2023
… use dot notation (#8437) This PR tests a string-based tool for renaming declarations. Inspired by [this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Renaming.20decls.20using.20LSP/near/402399853), I am trying to reduce the diff of #8406. This PR makes the following renames: | From | To |
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
mathlib-bors bot
pushed a commit
that referenced
this pull request
Nov 17, 2023
[Zulip](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.238406.20IsIntegral.20dot.20notation.2C.20noncomm.20generalization.20.26.20golf/near/402028285) Initially I just wanted to add more dot notations for IsIntegral and IsAlgebraic (done in #8437); then I noticed near-duplicates [Algebra.isIntegral_of_finite](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/IntegralClosure.html#Algebra.isIntegral_of_finite) `[Field R] [Ring A]` and [RingHom.IsIntegral.of_finite](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/IntegralClosure.html#RingHom.IsIntegral.of_finite) `[CommRing R] [CommRing A]` so I went on to generalize the latter to cover the former, and generalized everything in the IntegralClosure file to the noncommutative case whenever possible. In the process I noticed more golfs, which result in this PR. Most notably, [isIntegral_of_mem_of_FG](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/IntegralClosure.html#isIntegral_of_mem_of_FG) is now proven using [Cayley-Hamilton](https://math.stackexchange.com/a/2494433/12932) and doesn't depend on the Noetherian case [isIntegral_of_noetherian](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/IntegralClosure.html#isIntegral_of_noetherian); the latter is now proven using the former. In total the golfs makes mathlib 227 lines leaner (+487 -714). The main changes are in the single file [RingTheory/IntegralClosure](https://github.com/leanprover-community/mathlib4/pull/8406/files#diff-426d60d7e9edc9e20379127612410ad633864c2d5a9cd001729d128f0993b00e): + Change the definition of `Algebra.IsIntegral` which makes it unfold to `IsIntegral` rather than `RingHom.IsIntegralElem` because the former has much more APIs. + Fix lemma names involving `is_integral` which are actually about `IsIntegralElem`: `RingHom.is_integral_map` → `RingHom.isIntegralElem_map` `RingHom.is_integral_of_mem_closure` → `RingHom.IsIntegralElem.of_mem_closure` `RingHom.is_integral_zero/one` → `RingHom.isIntegralElem_zero/one` `RingHom.is_integral_add/neg/sub/mul/of_mul_unit` → `RingHom.IsIntegralElem.add/neg/sub/mul/of_mul_unit` + Add a lemma `Algebra.IsIntegral.of_injective`. + Move `isIntegral_of_(submodule_)noetherian` down and golf them. + Remove `(Algebra.)isIntegral_of_finite` that work only over fields, in favor of the more general `(Algebra.)isIntegral.of_finite`. + Merge duplicate lemmas `isIntegral_of_isScalarTower` and `isIntegral_tower_top_of_isIntegral` into `IsIntegral.tower_top`. + Golf `IsIntegral.of_mem_of_fg` by first proving `IsIntegral.of_finite` using Cayley-Hamilton. + Add a docstring mentioning the Kurosh problem at `Algebra.IsIntegral.finite`. The negative solution to the problem means the theorem doesn't generalize to noncommutative algebras. + Golf `IsIntegral.tmul` and `isField_of_isIntegral_of_isField(')`. + Combine `isIntegral_trans_aux` into `isIntegral_trans` and golf. + Add `Algebra` namespace to `isIntegral_sup`. + rename lemmas for dot notation: `RingHom.isIntegral_trans` → `RingHom.IsIntegral.trans` `RingHom.isIntegral_quotient/tower_bot/top_of_isIntegral` → `RingHom.IsIntegral.quotient/tower_bot/top` `isIntegral_of_mem_closure'` → `IsIntegral.of_mem_closure'` (and the '' version) `isIntegral_of_surjective` → `Algebra.isIntegral_of_surjective` The next changed file is RingTheory/Algebraic: + Rename: `of_larger_base` → `tower_top` (for consistency with `IsIntegral`) `Algebra.isAlgebraic_of_finite` → `Algebra.IsAlgebraic.of_finite` `Algebra.isAlgebraic_trans` → `Algebra.IsAlgebraic.trans` + Add new lemmas`Algebra.IsIntegral.isAlgebraic`, `isAlgebraic_algHom_iff`, and `Algebra.IsAlgebraic.of_injective` to streamline some proofs. The generalization from CommRing to Ring requires an additional lemma `scaleRoots_eval₂_mul_of_commute` in Polynomial/ScaleRoots. A lemma `Algebra.lmul_injective` is added to Algebra/Bilinear (in order to golf the proof of `IsIntegral.of_mem_of_fg`). In all other files, I merely fix the changed names, or use newly available dot notations. Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
alexkeizer
pushed a commit
that referenced
this pull request
Nov 17, 2023
… use dot notation (#8437) This PR tests a string-based tool for renaming declarations. Inspired by [this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Renaming.20decls.20using.20LSP/near/402399853), I am trying to reduce the diff of #8406. This PR makes the following renames: | From | To |
alexkeizer
pushed a commit
that referenced
this pull request
Nov 21, 2023
… use dot notation (#8437) This PR tests a string-based tool for renaming declarations. Inspired by [this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Renaming.20decls.20using.20LSP/near/402399853), I am trying to reduce the diff of #8406. This PR makes the following renames: | From | To |
alexkeizer
pushed a commit
that referenced
this pull request
Nov 21, 2023
[Zulip](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.238406.20IsIntegral.20dot.20notation.2C.20noncomm.20generalization.20.26.20golf/near/402028285) Initially I just wanted to add more dot notations for IsIntegral and IsAlgebraic (done in #8437); then I noticed near-duplicates [Algebra.isIntegral_of_finite](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/IntegralClosure.html#Algebra.isIntegral_of_finite) `[Field R] [Ring A]` and [RingHom.IsIntegral.of_finite](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/IntegralClosure.html#RingHom.IsIntegral.of_finite) `[CommRing R] [CommRing A]` so I went on to generalize the latter to cover the former, and generalized everything in the IntegralClosure file to the noncommutative case whenever possible. In the process I noticed more golfs, which result in this PR. Most notably, [isIntegral_of_mem_of_FG](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/IntegralClosure.html#isIntegral_of_mem_of_FG) is now proven using [Cayley-Hamilton](https://math.stackexchange.com/a/2494433/12932) and doesn't depend on the Noetherian case [isIntegral_of_noetherian](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/IntegralClosure.html#isIntegral_of_noetherian); the latter is now proven using the former. In total the golfs makes mathlib 227 lines leaner (+487 -714). The main changes are in the single file [RingTheory/IntegralClosure](https://github.com/leanprover-community/mathlib4/pull/8406/files#diff-426d60d7e9edc9e20379127612410ad633864c2d5a9cd001729d128f0993b00e): + Change the definition of `Algebra.IsIntegral` which makes it unfold to `IsIntegral` rather than `RingHom.IsIntegralElem` because the former has much more APIs. + Fix lemma names involving `is_integral` which are actually about `IsIntegralElem`: `RingHom.is_integral_map` → `RingHom.isIntegralElem_map` `RingHom.is_integral_of_mem_closure` → `RingHom.IsIntegralElem.of_mem_closure` `RingHom.is_integral_zero/one` → `RingHom.isIntegralElem_zero/one` `RingHom.is_integral_add/neg/sub/mul/of_mul_unit` → `RingHom.IsIntegralElem.add/neg/sub/mul/of_mul_unit` + Add a lemma `Algebra.IsIntegral.of_injective`. + Move `isIntegral_of_(submodule_)noetherian` down and golf them. + Remove `(Algebra.)isIntegral_of_finite` that work only over fields, in favor of the more general `(Algebra.)isIntegral.of_finite`. + Merge duplicate lemmas `isIntegral_of_isScalarTower` and `isIntegral_tower_top_of_isIntegral` into `IsIntegral.tower_top`. + Golf `IsIntegral.of_mem_of_fg` by first proving `IsIntegral.of_finite` using Cayley-Hamilton. + Add a docstring mentioning the Kurosh problem at `Algebra.IsIntegral.finite`. The negative solution to the problem means the theorem doesn't generalize to noncommutative algebras. + Golf `IsIntegral.tmul` and `isField_of_isIntegral_of_isField(')`. + Combine `isIntegral_trans_aux` into `isIntegral_trans` and golf. + Add `Algebra` namespace to `isIntegral_sup`. + rename lemmas for dot notation: `RingHom.isIntegral_trans` → `RingHom.IsIntegral.trans` `RingHom.isIntegral_quotient/tower_bot/top_of_isIntegral` → `RingHom.IsIntegral.quotient/tower_bot/top` `isIntegral_of_mem_closure'` → `IsIntegral.of_mem_closure'` (and the '' version) `isIntegral_of_surjective` → `Algebra.isIntegral_of_surjective` The next changed file is RingTheory/Algebraic: + Rename: `of_larger_base` → `tower_top` (for consistency with `IsIntegral`) `Algebra.isAlgebraic_of_finite` → `Algebra.IsAlgebraic.of_finite` `Algebra.isAlgebraic_trans` → `Algebra.IsAlgebraic.trans` + Add new lemmas`Algebra.IsIntegral.isAlgebraic`, `isAlgebraic_algHom_iff`, and `Algebra.IsAlgebraic.of_injective` to streamline some proofs. The generalization from CommRing to Ring requires an additional lemma `scaleRoots_eval₂_mul_of_commute` in Polynomial/ScaleRoots. A lemma `Algebra.lmul_injective` is added to Algebra/Bilinear (in order to golf the proof of `IsIntegral.of_mem_of_fg`). In all other files, I merely fix the changed names, or use newly available dot notations. Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
grunweg
pushed a commit
that referenced
this pull request
Dec 15, 2023
… use dot notation (#8437) This PR tests a string-based tool for renaming declarations. Inspired by [this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Renaming.20decls.20using.20LSP/near/402399853), I am trying to reduce the diff of #8406. This PR makes the following renames: | From | To |
grunweg
pushed a commit
that referenced
this pull request
Dec 15, 2023
[Zulip](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.238406.20IsIntegral.20dot.20notation.2C.20noncomm.20generalization.20.26.20golf/near/402028285) Initially I just wanted to add more dot notations for IsIntegral and IsAlgebraic (done in #8437); then I noticed near-duplicates [Algebra.isIntegral_of_finite](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/IntegralClosure.html#Algebra.isIntegral_of_finite) `[Field R] [Ring A]` and [RingHom.IsIntegral.of_finite](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/IntegralClosure.html#RingHom.IsIntegral.of_finite) `[CommRing R] [CommRing A]` so I went on to generalize the latter to cover the former, and generalized everything in the IntegralClosure file to the noncommutative case whenever possible. In the process I noticed more golfs, which result in this PR. Most notably, [isIntegral_of_mem_of_FG](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/IntegralClosure.html#isIntegral_of_mem_of_FG) is now proven using [Cayley-Hamilton](https://math.stackexchange.com/a/2494433/12932) and doesn't depend on the Noetherian case [isIntegral_of_noetherian](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/IntegralClosure.html#isIntegral_of_noetherian); the latter is now proven using the former. In total the golfs makes mathlib 227 lines leaner (+487 -714). The main changes are in the single file [RingTheory/IntegralClosure](https://github.com/leanprover-community/mathlib4/pull/8406/files#diff-426d60d7e9edc9e20379127612410ad633864c2d5a9cd001729d128f0993b00e): + Change the definition of `Algebra.IsIntegral` which makes it unfold to `IsIntegral` rather than `RingHom.IsIntegralElem` because the former has much more APIs. + Fix lemma names involving `is_integral` which are actually about `IsIntegralElem`: `RingHom.is_integral_map` → `RingHom.isIntegralElem_map` `RingHom.is_integral_of_mem_closure` → `RingHom.IsIntegralElem.of_mem_closure` `RingHom.is_integral_zero/one` → `RingHom.isIntegralElem_zero/one` `RingHom.is_integral_add/neg/sub/mul/of_mul_unit` → `RingHom.IsIntegralElem.add/neg/sub/mul/of_mul_unit` + Add a lemma `Algebra.IsIntegral.of_injective`. + Move `isIntegral_of_(submodule_)noetherian` down and golf them. + Remove `(Algebra.)isIntegral_of_finite` that work only over fields, in favor of the more general `(Algebra.)isIntegral.of_finite`. + Merge duplicate lemmas `isIntegral_of_isScalarTower` and `isIntegral_tower_top_of_isIntegral` into `IsIntegral.tower_top`. + Golf `IsIntegral.of_mem_of_fg` by first proving `IsIntegral.of_finite` using Cayley-Hamilton. + Add a docstring mentioning the Kurosh problem at `Algebra.IsIntegral.finite`. The negative solution to the problem means the theorem doesn't generalize to noncommutative algebras. + Golf `IsIntegral.tmul` and `isField_of_isIntegral_of_isField(')`. + Combine `isIntegral_trans_aux` into `isIntegral_trans` and golf. + Add `Algebra` namespace to `isIntegral_sup`. + rename lemmas for dot notation: `RingHom.isIntegral_trans` → `RingHom.IsIntegral.trans` `RingHom.isIntegral_quotient/tower_bot/top_of_isIntegral` → `RingHom.IsIntegral.quotient/tower_bot/top` `isIntegral_of_mem_closure'` → `IsIntegral.of_mem_closure'` (and the '' version) `isIntegral_of_surjective` → `Algebra.isIntegral_of_surjective` The next changed file is RingTheory/Algebraic: + Rename: `of_larger_base` → `tower_top` (for consistency with `IsIntegral`) `Algebra.isAlgebraic_of_finite` → `Algebra.IsAlgebraic.of_finite` `Algebra.isAlgebraic_trans` → `Algebra.IsAlgebraic.trans` + Add new lemmas`Algebra.IsIntegral.isAlgebraic`, `isAlgebraic_algHom_iff`, and `Algebra.IsAlgebraic.of_injective` to streamline some proofs. The generalization from CommRing to Ring requires an additional lemma `scaleRoots_eval₂_mul_of_commute` in Polynomial/ScaleRoots. A lemma `Algebra.lmul_injective` is added to Algebra/Bilinear (in order to golf the proof of `IsIntegral.of_mem_of_fg`). In all other files, I merely fix the changed names, or use newly available dot notations. Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR tests a string-based tool for renaming declarations.
Inspired by this Zulip thread, I am trying to reduce the diff of #8406.
This PR makes the following renames:
FG_adjoin_singleton_of_integralIsIntegral.fg_adjoin_singletonFG_adjoin_of_finitefg_adjoin_of_finiteisIntegral_quotient_of_isIntegralAlgebra.IsIntegral.quotientisAlgebraic_of_larger_base_of_injectiveIsAlgebraic.of_larger_base_of_injectiveisAlgebraic_of_powIsAlgebraic.of_powisAlgebraic_algHom_of_isAlgebraicIsAlgebraic.algHomisAlgebraic_algebraMap_of_isAlgebraicIsAlgebraic.algebraMapisAlgebraic_of_finiteIsAlgebraic.of_finiteisAlgebraic_of_larger_baseIsAlgebraic.of_larger_baseisIntegral_addIsIntegral.addisIntegral_map_of_comp_eq_of_isIntegralIsIntegral.map_of_comp_eqisIntegral_mulIsIntegral.mulisIntegral_negIsIntegral.negisIntegral_ofSubringIsIntegral.of_subringisIntegral_of_finiteIsIntegral.of_finiteisIntegral_of_isIntegral_mul_unitIsIntegral.of_mul_unitisIntegral_of_mem_closureIsIntegral.of_mem_closureisIntegral_of_mem_of_FGIsIntegral.of_mem_of_fgisIntegral_of_powIsIntegral.of_powisIntegral_smulIsIntegral.smulisIntegral_subIsIntegral.subisIntegral_tower_bot_of_isIntegralIsIntegral.tower_botisIntegral_tower_bot_of_isIntegral_fieldIsIntegral.tower_bot_of_fieldmap_isIntegralIsIntegral.mapmem_integralClosure_iff_mem_FGmem_integralClosure_iff_mem_fgAffected files: