Just out of curiosity, what is the logic behind the use of the A/B/C letters in lemmas such as `addnBCA`

? There must be one, but it is not right away obvious to me. A similar question arises with A/B and `subn...`

names. Thanks.

see here: https://github.com/math-comp/math-comp/blob/master/CONTRIBUTING.md#where

we managed to get quite good naming prediction rates from theorem statements with neural machine learning, which probably says something about the MathComp naming schemes being quite robust

Last updated: Jan 29 2023 at 19:02 UTC