[Merged by Bors] - feat(RingTheory/Localization/*): add `IsLocalization.algEquivOfAlgEquiv` and other results by acmepjz · Pull Request #18661 · leanprover-community/mathlib4

acmepjz · 2024-11-05T15:30:16Z

MulEquivClass.map_nonZeroDivisors: MulEquiv preserves non-zero divisors
IsLocalization.algEquivOfAlgEquiv: generalizes IsLocalization.ringEquivOfRingEquiv
rename IsFractionRing.fieldEquivOfRingEquiv -> IsFractionRing.ringEquivOfRingEquiv as it does not require field assumption anymore
IsFractionRing.algEquivOfAlgEquiv: generalize IsFractionRing.ringEquivOfRingEquiv
IsLocalization.liftAlgHom, IsFractionRing.liftAlgHom: AlgHom version of lift
generalize FractionRing.algEquiv to ring case
remove IsDomain assumption as much as possible. This makes the left hand side of mk'_eq_zero_iff_eq_zero not a simp normal form, so it's removed from simp lemmas.

github-actions · 2024-11-05T15:31:14Z

PR summary 36bca67931

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ MulEquivClass.map_nonZeroDivisors
+ algEquivOfAlgEquiv_algebraMap
+ algEquivOfAlgEquiv_eq
+ algEquivOfAlgEquiv_eq_map
+ algEquivOfAlgEquiv_mk'
+ restrictScalars_fieldEquivOfAlgEquiv
+ ringEquivOfRingEquiv
+ ringEquivOfRingEquiv_algebraMap
++ algEquivOfAlgEquiv
++ algEquivOfAlgEquiv_symm
++ coe_liftAlgHom
++ liftAlgHom
++ liftAlgHom_apply
++ liftAlgHom_toRingHom
++ ringEquivOfRingEquiv_symm

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.

Mathlib/RingTheory/Localization/Basic.lean

Mathlib/RingTheory/Localization/FractionRing.lean

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Mathlib/RingTheory/Localization/FractionRing.lean

Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean

Mathlib/RingTheory/Localization/Basic.lean

Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

alreadydone

Thanks!
maintainer merge

github-actions · 2024-11-13T12:20:08Z

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

riccardobrasca · 2024-11-13T12:39:25Z

Thanks!

bors merge

…iv` and other results (#18661) - `MulEquivClass.map_nonZeroDivisors`: `MulEquiv` preserves non-zero divisors - `IsLocalization.algEquivOfAlgEquiv`: generalizes `IsLocalization.ringEquivOfRingEquiv` - rename `IsFractionRing.fieldEquivOfRingEquiv` -> `IsFractionRing.ringEquivOfRingEquiv` as it does not require field assumption anymore - `IsFractionRing.algEquivOfAlgEquiv`: generalize `IsFractionRing.ringEquivOfRingEquiv` - `IsLocalization.liftAlgHom`, `IsFractionRing.liftAlgHom`: `AlgHom` version of `lift` - generalize `FractionRing.algEquiv` to ring case - remove `IsDomain` assumption as much as possible. This makes the left hand side of `mk'_eq_zero_iff_eq_zero` not a simp normal form, so it's removed from simp lemmas.

mathlib-bors · 2024-11-13T12:54:14Z

Build failed:

Build

riccardobrasca · 2024-11-13T13:01:08Z

Can you please merge master and fix the error? Thanks!

bors d+

mathlib-bors · 2024-11-13T13:01:10Z

✌️ acmepjz can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

alreadydone · 2024-11-13T13:19:37Z

Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean

+  ext
+  simp_rw [Submonoid.map_equiv_eq_comap_symm, Submonoid.mem_comap, mem_nonZeroDivisors_iff,
+    ← h.symm.forall_congr_right, h.symm.coe_toMonoidHom, h.symm.toEquiv_eq_coe, h.symm.coe_toEquiv,
+    ← map_mul, map_eq_zero_iff _ h.symm.injective]


looks like to_additive alias malfunctioing in #18809 ...

riccardobrasca · 2024-11-13T14:22:16Z

Thanks!

bors merge

…iv` and other results (#18661) - `MulEquivClass.map_nonZeroDivisors`: `MulEquiv` preserves non-zero divisors - `IsLocalization.algEquivOfAlgEquiv`: generalizes `IsLocalization.ringEquivOfRingEquiv` - rename `IsFractionRing.fieldEquivOfRingEquiv` -> `IsFractionRing.ringEquivOfRingEquiv` as it does not require field assumption anymore - `IsFractionRing.algEquivOfAlgEquiv`: generalize `IsFractionRing.ringEquivOfRingEquiv` - `IsLocalization.liftAlgHom`, `IsFractionRing.liftAlgHom`: `AlgHom` version of `lift` - generalize `FractionRing.algEquiv` to ring case - remove `IsDomain` assumption as much as possible. This makes the left hand side of `mk'_eq_zero_iff_eq_zero` not a simp normal form, so it's removed from simp lemmas. Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

mathlib-bors · 2024-11-13T15:19:29Z

Pull request successfully merged into master.

Build succeeded:

acmepjz · 2024-11-13T16:27:30Z

Can you please merge master and fix the error? Thanks!

Sorry, I was AFK for a while. Thanks for fixing the problem.

…iv` and other results (#18661) - `MulEquivClass.map_nonZeroDivisors`: `MulEquiv` preserves non-zero divisors - `IsLocalization.algEquivOfAlgEquiv`: generalizes `IsLocalization.ringEquivOfRingEquiv` - rename `IsFractionRing.fieldEquivOfRingEquiv` -> `IsFractionRing.ringEquivOfRingEquiv` as it does not require field assumption anymore - `IsFractionRing.algEquivOfAlgEquiv`: generalize `IsFractionRing.ringEquivOfRingEquiv` - `IsLocalization.liftAlgHom`, `IsFractionRing.liftAlgHom`: `AlgHom` version of `lift` - generalize `FractionRing.algEquiv` to ring case - remove `IsDomain` assumption as much as possible. This makes the left hand side of `mk'_eq_zero_iff_eq_zero` not a simp normal form, so it's removed from simp lemmas. Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

add IsLocalization.algEquivOfAlgEquiv and other results

d21b6a9

acmepjz added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-algebra Algebra (groups, rings, fields, etc) labels Nov 5, 2024

acmepjz mentioned this pull request Nov 5, 2024

[Merged by Bors] - feat(RingTheory/AlgebraicIndependent): add AlgebraicIndependent.aevalEquivField and other results #18648

Closed

2 tasks

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Nov 5, 2024

acmepjz added 7 commits November 6, 2024 12:06

fix date

fa8f074

remove IsDomain A assumption as much as possible

e289cd0

fix

69ff50a

??

5dcc2e4

remove [simp]

f065eb9

add liftAlgHom

2b6cbd9

fix

2668585

acmepjz mentioned this pull request Nov 8, 2024

[Merged by Bors] - feat: some results on dimension of field adjoin #18515

Closed

erdOne reviewed Nov 9, 2024

View reviewed changes

erdOne added the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 9, 2024

acmepjz and others added 4 commits November 10, 2024 00:28

Apply suggestions from code review

b86d2c5

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

add algEquivOfAlgEquiv_symm

7cc13a0

fix docstring

a52cd64

apply suggestions

f9076d4

acmepjz removed the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 9, 2024

acmepjz added 3 commits November 10, 2024 01:07

fix

641890e

remove a simp lemma

1c944ae

Merge branch 'master' into acmepjz_alg_equiv_of_alg_equiv

7b4d032

acmepjz requested a review from alreadydone November 12, 2024 18:25

alreadydone approved these changes Nov 12, 2024

View reviewed changes

Mathlib/RingTheory/Localization/FractionRing.lean Outdated Show resolved Hide resolved

Mathlib/RingTheory/Localization/FractionRing.lean Outdated Show resolved Hide resolved

Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean Outdated Show resolved Hide resolved

alreadydone reviewed Nov 12, 2024

View reviewed changes

Mathlib/RingTheory/Localization/Basic.lean Outdated Show resolved Hide resolved

acmepjz and others added 2 commits November 13, 2024 07:52

Apply suggestions from code review

05fca98

Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

apply suggestions

2a7f163

alreadydone approved these changes Nov 13, 2024

View reviewed changes

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Nov 13, 2024

github-actions bot added the ready-to-merge This PR has been sent to bors. label Nov 13, 2024

github-actions bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Nov 13, 2024

alreadydone reviewed Nov 13, 2024

View reviewed changes

alreadydone added 2 commits November 13, 2024 08:43

Merge branch 'master' into acmepjz_alg_equiv_of_alg_equiv

4089038

move aliases below def of MulEquivClass

36bca67

alreadydone added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Nov 13, 2024

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Nov 13, 2024

mathlib-bors bot changed the title ~~feat(RingTheory/Localization/*): add IsLocalization.algEquivOfAlgEquiv and other results~~ [Merged by Bors] - feat(RingTheory/Localization/*): add IsLocalization.algEquivOfAlgEquiv and other results Nov 13, 2024

mathlib-bors bot closed this Nov 13, 2024

mathlib-bors bot deleted the acmepjz_alg_equiv_of_alg_equiv branch November 13, 2024 15:19

Conversation

acmepjz commented Nov 5, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Nov 5, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 36bca67931

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

alreadydone left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Nov 13, 2024

Uh oh!

riccardobrasca commented Nov 13, 2024

Uh oh!

mathlib-bors bot commented Nov 13, 2024

Uh oh!

riccardobrasca commented Nov 13, 2024

Uh oh!

mathlib-bors bot commented Nov 13, 2024

Uh oh!

alreadydone Nov 13, 2024

Choose a reason for hiding this comment

Uh oh!

riccardobrasca commented Nov 13, 2024

Uh oh!

mathlib-bors bot commented Nov 13, 2024

Uh oh!

acmepjz commented Nov 13, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

acmepjz commented Nov 5, 2024 •

edited

Loading

github-actions bot commented Nov 5, 2024 •

edited

Loading