search

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
378 stars 22 forks source link

"ad" is not defined #194

Open ncfavier opened 1 year ago

ncfavier commented 1 year ago

$\mathrm{ad}$ is used here:

https://github.com/UniMath/SymmetryBook/blob/33011ebf1fc139cc6f17ab45b5f8db7ae4b4a00a/group.tex#L2356

But is not defined. I guess it means conjugation?

pierrecagne commented 1 year ago

Indeed, this 'ad' has been deprecated. It should be $\Omega \Bf$ now according to Def 4.4.5.