fix xca:ints-as-quotient and lem:euclid-div, clarify lem:PHP

UniMath / SymmetryBook

This book will be an undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.

Creative Commons Attribution Share Alike 4.0 International

371 stars 22 forks source link

fix xca:ints-as-quotient and lem:euclid-div, clarify lem:PHP #192

Open clayrat opened 11 months ago

clayrat commented 11 months ago

Exercise 2.22.14 omits p in the final equation and has tuple brackets in the wrong order.
Lemma 2.23.6 has n in two different meanings which is somewhat confusing, I renamed the first instance to x.
Lemma 2.23.8 refers to mu_P(n), however Construction 2.23.4 returns mu_P(n+1)