[Merged by Bors] - feat: add definition of opposite of subsemirings, subrings, and subalgebras by acmepjz · Pull Request #12846 · leanprover-community/mathlib4

acmepjz · 2024-05-12T16:31:30Z

similar to that in Mathlib.Algebra.Group.Subgroup.MulOpposite

discussion: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Subalgebra.2EequivOpposite

eric-wieser · 2024-05-12T18:03:23Z

Can you copy the Submonoid.MulOpposite file here instead, and build up separate op and unop definitions?

acmepjz · 2024-05-12T18:14:05Z

Can you copy the Submonoid.MulOpposite file here instead, and build up separate op and unop definitions?

Let me check later.

acmepjz · 2024-05-19T00:24:17Z

Can you copy the Submonoid.MulOpposite file here instead, and build up separate op and unop definitions?

Done.

Mathlib/Algebra/Algebra/Subalgebra/MulOpposite.lean

YaelDillies · 2024-06-17T10:10:21Z

Mathlib/Algebra/Algebra/Subalgebra/MulOpposite.lean

+
+/-- A subalgebra `S` of `A / R` determines a subring `S.op` of the opposite ring `Aᵐᵒᵖ / R`. -/
+@[simps]
+def opEquiv : Subalgebra R A ≃o Subalgebra R Aᵐᵒᵖ where


Suggested change

def opEquiv : Subalgebra R A ≃o Subalgebra R Aᵐᵒᵖ where

def opOrderIso : Subalgebra R A ≃o Subalgebra R Aᵐᵒᵖ where

But it's called Submonoid.opEquiv for Submonoid, etc.

Uh, okay 😦

github-actions · 2024-06-17T19:06:16Z

PR summary 0f07e4166a

Import changes

No significant changes to the import graph

Declarations diff

+ algEquivOpMop
+ linearEquivOp
+ mopAlgEquivOp
+ op_adjoin
+ op_toSubring
+ unop_adjoin
+ unop_toSubring
++ addEquivOp
++ mopRingEquivOp
++ op_closure
++ ringEquivOpMop
++ unop_closure
+++ le_op_iff
+++ mem_op
+++ mem_unop
+++ op
+++ opEquiv
+++ op_bot
+++ op_coe
+++ op_iInf
+++ op_iSup
+++ op_inf
+++ op_le_iff
+++ op_le_op_iff
+++ op_sInf
+++ op_sSup
+++ op_sup
+++ op_top
+++ op_unop
+++ unop
+++ unop_bot
+++ unop_coe
+++ unop_iInf
+++ unop_iSup
+++ unop_inf
+++ unop_le_unop_iff
+++ unop_op
+++ unop_sInf
+++ unop_sSup
+++ unop_sup
+++ unop_top

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

YaelDillies · 2024-06-17T20:42:52Z

Thanks!

maintainer merge

github-actions · 2024-06-17T20:43:08Z

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

eric-wieser · 2024-06-17T23:43:54Z

Mathlib/Algebra/Ring/Subsemiring/MulOpposite.lean

+
+namespace Subsemiring
+
+variable {ι R : Type*} [NonAssocSemiring R]


ι should be a Sort*

eric-wieser

Just the ι issue to solve (in all three files)

eric-wieser

bors d+

thanks!

mathlib-bors · 2024-06-18T00:02:32Z

✌️ 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.

acmepjz · 2024-06-18T00:39:10Z

bors r+

…gebras (#12846) similar to that in `Mathlib.Algebra.Group.Subgroup.MulOpposite`

mathlib-bors · 2024-06-18T00:49:58Z

Pull request successfully merged into master.

Build succeeded:

…gebras (#12846) similar to that in `Mathlib.Algebra.Group.Subgroup.MulOpposite`

add definition of opposite of subalgebras

fa92742

acmepjz added awaiting-review 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 May 12, 2024

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

acmepjz added a commit that referenced this pull request May 12, 2024

adapt #12846 and move some results

42ea134

acmepjz added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels May 12, 2024

acmepjz mentioned this pull request May 12, 2024

[Merged by Bors] - feat(FieldTheory/LinearDisjoint): definition and basic properties of linearly disjoint of fields #9651

Closed

14 tasks

acmepjz added 2 commits May 19, 2024 03:49

Merge branch 'master' into acmepjz_subalg_op

e11804b

add two more files

795270b

acmepjz added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels May 19, 2024

acmepjz changed the title ~~feat(Algebra/Algebra/Subalgebra/MulOpposite): add definition of opposite of subalgebras~~ feat: add definition of opposite of subsemirings, subrings, and subalgebras May 19, 2024

YaelDillies reviewed Jun 17, 2024

View reviewed changes

YaelDillies added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jun 17, 2024

acmepjz added 2 commits June 18, 2024 03:01

Merge branch 'master' into acmepjz_subalg_op

6fcfb0c

apply suggestions

2740c87

acmepjz added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jun 17, 2024

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

eric-wieser reviewed Jun 17, 2024

View reviewed changes

eric-wieser approved these changes Jun 17, 2024

View reviewed changes

apply suggestions

0f07e41

eric-wieser approved these changes Jun 18, 2024

View reviewed changes

ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Jun 18, 2024

eric-wieser added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 18, 2024

acmepjz removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 18, 2024

mathlib-bors bot pushed a commit that referenced this pull request Jun 18, 2024

feat: add definition of opposite of subsemirings, subrings, and subal…

1db89cb

…gebras (#12846) similar to that in `Mathlib.Algebra.Group.Subgroup.MulOpposite`

mathlib-bors bot changed the title ~~feat: add definition of opposite of subsemirings, subrings, and subalgebras~~ [Merged by Bors] - feat: add definition of opposite of subsemirings, subrings, and subalgebras Jun 18, 2024

mathlib-bors bot closed this Jun 18, 2024

mathlib-bors bot deleted the acmepjz_subalg_op branch June 18, 2024 00:50

AntoineChambert-Loir pushed a commit that referenced this pull request Jun 20, 2024

feat: add definition of opposite of subsemirings, subrings, and subal…

45809b5

…gebras (#12846) similar to that in `Mathlib.Algebra.Group.Subgroup.MulOpposite`

grunweg pushed a commit that referenced this pull request Jun 20, 2024

feat: add definition of opposite of subsemirings, subrings, and subal…

e4db5d1

…gebras (#12846) similar to that in `Mathlib.Algebra.Group.Subgroup.MulOpposite`

kbuzzard pushed a commit that referenced this pull request Jun 26, 2024

feat: add definition of opposite of subsemirings, subrings, and subal…

fa1c7cc

…gebras (#12846) similar to that in `Mathlib.Algebra.Group.Subgroup.MulOpposite`

	def opEquiv : Subalgebra R A ≃o Subalgebra R Aᵐᵒᵖ where
	def opOrderIso : Subalgebra R A ≃o Subalgebra R Aᵐᵒᵖ where


		namespace Subsemiring

		variable {ι R : Type*} [NonAssocSemiring R]

Conversation

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

Uh oh!

Uh oh!

eric-wieser commented May 12, 2024

Uh oh!

acmepjz commented May 12, 2024

Uh oh!

acmepjz commented May 19, 2024

Uh oh!

Uh oh!

Uh oh!

YaelDillies Jun 17, 2024

Choose a reason for hiding this comment

Uh oh!

acmepjz Jun 17, 2024

Choose a reason for hiding this comment

Uh oh!

YaelDillies Jun 17, 2024

Choose a reason for hiding this comment

Uh oh!

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

Uh oh!

PR summary 0f07e4166a

Import changes

Declarations diff

Uh oh!

YaelDillies commented Jun 17, 2024

Uh oh!

github-actions bot commented Jun 17, 2024

Uh oh!

eric-wieser Jun 17, 2024

Choose a reason for hiding this comment

Uh oh!

acmepjz Jun 17, 2024

Choose a reason for hiding this comment

Uh oh!

eric-wieser left a comment

Choose a reason for hiding this comment

Uh oh!

eric-wieser left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Jun 18, 2024

Uh oh!

acmepjz commented Jun 18, 2024

Uh oh!

mathlib-bors bot commented Jun 18, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

acmepjz commented May 12, 2024 •

edited

Loading

github-actions bot commented Jun 17, 2024 •

edited

Loading