Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

opposite rings #1940

Merged
merged 13 commits into from
May 2, 2024
Merged

opposite rings #1940

Changes from 1 commit
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
b0c83eb
opposite rings
Alizter Apr 30, 2024
bf73db5
Update theories/Classes/theory/groups.v
Alizter Apr 30, 2024
7cf29dc
Update theories/Classes/theory/groups.v
Alizter Apr 30, 2024
a7a07aa
it gets weirder
Alizter May 1, 2024
42f43aa
update comment in test
Alizter May 1, 2024
5a5f22a
redefine right ideals over opposite ring
Alizter May 2, 2024
b76f725
update tests with cring_op
Alizter May 2, 2024
828ebe5
Merge branch 'master' into ps/rr/opposite_rings
Alizter May 2, 2024
0841755
Rings/Ideal: fix typo and clarify comment
jdchristensen May 2, 2024
57d4f02
remove opposite commutative ring (its the same ring and rng_op works)
Alizter May 2, 2024
448539a
Groups/Subgroup: add functor_subgroup_generated
jdchristensen May 2, 2024
53e4cda
Rings/Ideal: remove most duplication from isrightideal_ideal_product_…
jdchristensen May 2, 2024
2388bc6
reverse order of arguments to ring_mult_assoc_opp
Alizter May 2, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 12 additions & 0 deletions test/Algebra/Rings/Ring.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,3 +7,15 @@ Local Open Scope path_scope.
(** Test that opposite rings are definitionally involutive. *)
Definition test1 (R : Ring) : R = (rng_op (rng_op R)) :> Ring := 1.
Definition test2 (R : CRing) : R = (rng_op (rng_op R)) :> CRing := 1.
Alizter marked this conversation as resolved.
Show resolved Hide resolved

Axiom fake_comm : forall (R : CRing) (x y : R), x * y = y * x.
Definition augment (R : CRing) : CRing.
Proof.
snrapply Build_CRing.
- exact R.
- exact (fake_comm R).
Defined.

Fail Definition test3 (R : CRing) : R = augment R :> CRing := 1.
(* !? *)
Definition test4 (R : CRing) : R = (rng_op (rng_op (augment R))) :> CRing := 1.
Alizter marked this conversation as resolved.
Show resolved Hide resolved
Loading