Code

switch to Int in cring_Z#2000

Code

Merged

Alizter merged 15 commits intoHoTT:masterHoTT/Coq-HoTT:masterfrom Alizter:ps/rr/switch_to_int_in_cring_zAlizter/HoTT:ps/rr/switch_to_int_in_cring_zCopy head branch name to clipboardJul 5, 2024

+377-396

Commits

Commits on Jun 28, 2024

• switch to Int in cring_Z

  Show description for 109eea1
  Alizter

  committed
  109eea1

• fix test

  Show description for 9bfde56
  Alizter

  committed
  9bfde56

• Commuting lemma for int_iter

  ThomatoTomato

  committed
  2a34b75

• simplify int_iter_comm

  Show description for 1398764
  Alizter

  committed
  1398764

Commits on Jun 29, 2024

• Rings/Z.v, Int.v: some cleanups

  jdchristensen

  committed
  f91be4c

• Int.v: generalize/rename int_iter_commute_map and use twice

  jdchristensen

  committed
  0c92bcd

• generalse rng_int_mult to arb elements and split IsMonoidPres proof

  Show description for 061a7ad
  Alizter

  committed
  061a7ad

Commits on Jun 30, 2024

• Rings/Z.v: generalize results about rng_int_mult; update comments

  jdchristensen

  committed
  47f2da2

• generalise and move rng_int_mult for abgroup

  Show description for c125988
  Alizter

  committed
  c125988

• remove comment about switching to int as this has been done

  Show description for be2de28
  Alizter

  committed
  be2de28

• Various cleanups to grp_pow, ab_mul, abgroup_int_mult and rng_int_mult

  jdchristensen

  committed
  1ba97c8

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

  jdchristensen

  authored
  4e36937

Commits on Jul 2, 2024

• Algebra/*: Use int_iter for grp_pow

  jdchristensen

  committed
  0eb2643

• Algebra: rename grp_pow_* and reorder one result

  jdchristensen

  committed
  43e08df

Commits on Jul 3, 2024

• AbGroups/Z: get rid of abgroup_int_mult

  jdchristensen

  committed
  1e60610