Code

opposite rings#1940

Code

Merged

Alizter merged 13 commits intoHoTT:masterHoTT/Coq-HoTT:masterfrom Alizter:ps/rr/opposite_ringsAlizter/HoTT:ps/rr/opposite_ringsCopy head branch name to clipboardMay 2, 2024

+340-356

Commits

Commits on Apr 30, 2024

• opposite rings

  Show description for b0c83eb
  Alizter

  committed
  b0c83eb

  Copy full SHA for b0c83eb

• Update theories/Classes/theory/groups.v

  Alizter

  authored
  bf73db5

  Copy full SHA for bf73db5

• Update theories/Classes/theory/groups.v

  Alizter

  authored
  7cf29dc

  Copy full SHA for 7cf29dc

Commits on May 1, 2024

• it gets weirder

  Show description for a7a07aa
  Alizter

  committed
  a7a07aa

  Copy full SHA for a7a07aa

• update comment in test

  Show description for 42f43aa
  Alizter

  committed
  42f43aa

  Copy full SHA for 42f43aa

Commits on May 2, 2024

• redefine right ideals over opposite ring

  Show description for 5a5f22a
  Alizter

  committed
  5a5f22a

  Copy full SHA for 5a5f22a

• update tests with cring_op

  Show description for b76f725
  Alizter

  committed
  b76f725

  Copy full SHA for b76f725

• Merge branch 'master' into ps/rr/opposite_rings

  Alizter

  authored
  828ebe5

  Copy full SHA for 828ebe5

• Rings/Ideal: fix typo and clarify comment

  jdchristensen

  committed
  0841755

  Copy full SHA for 0841755

• remove opposite commutative ring (its the same ring and rng_op works)

  Show description for 57d4f02
  Alizter

  committed
  57d4f02

  Copy full SHA for 57d4f02

• Groups/Subgroup: add functor_subgroup_generated

  jdchristensen

  committed
  448539a

  Copy full SHA for 448539a

• Rings/Ideal: remove most duplication from isrightideal_ideal_product_type

  jdchristensen

  committed
  53e4cda

  Copy full SHA for 53e4cda

• reverse order of arguments to ring_mult_assoc_opp

  Show description for 2388bc6
  Alizter

  committed
  2388bc6

  Copy full SHA for 2388bc6