Code

integer group powers#1995

Code

Merged

jdchristensen merged 8 commits intoHoTT:masterHoTT/Coq-HoTT:masterfrom Alizter:ps/rr/integer_group_powersAlizter/HoTT:ps/rr/integer_group_powersCopy head branch name to clipboardJun 15, 2024

+138-72

Commits

Commits on Jun 12, 2024

• integer group powers

  Show description for b5d5cdb
  Alizter

  committed
  b5d5cdb

  Copy full SHA for b5d5cdb

• Changed grp_pow, and proved grp_pow_int_add

  ThomatoTomato

  committed
  7094f9e

  Copy full SHA for 7094f9e

Commits on Jun 13, 2024

• Changed grp_pow to Dan's suggestion

  ThomatoTomato

  committed
  7d2fe0b

  Copy full SHA for 7d2fe0b

• Completed ab_mul, changed grp_pow according to Dan's suggestion, and fixed broken definitions

  ThomatoTomato

  committed
  21fc2b9

  Copy full SHA for 21fc2b9

Commits on Jun 14, 2024

• cleanup

  ThomatoTomato

  committed
  89cb058

  Copy full SHA for 89cb058

• Remove free-standing comments

  Show description for 56f64b9
  

  ThomatoTomato

  and

  jdchristensen

  authored
  56f64b9

  Copy full SHA for 56f64b9

• Less parentheses

  Show description for bb24a47
  

  ThomatoTomato

  and

  jdchristensen

  authored
  bb24a47

  Copy full SHA for bb24a47

• cleanup, pt. 2

  ThomatoTomato

  committed
  478cc6f

  Copy full SHA for 478cc6f