to addtitive

Stream: general

[Anatole Dedecker]

Just being curious here : how does the to_additive attribute work ? For exemple, does it adapt the whole proof or does it use some lemmas to go back and forth between multiplicative and additive groups ? If we define a concept for multiplicative group, is there a way to tell "when using to_additive, it corresponds to this particular additive concept" ?

[Anatole Dedecker]

And if you have any other interesting things to know about this I'm interested too

[Scott Morrison]

It adapts the whole proof. It progressively builds a dictionary between multiplicative and additive declarations, and uses this to rewrite. It then adds the new declaration to the dictionary. It's also possible to add dictionary entries "after the fact", for occasions when the automatic adaptation fails, but you'd still like future adaptations to be able to make the translation.