to_additive documentation

Stream: general

[Eric Rodriguez]

in here I raised the question about what is the standard for documentations of to_additive things - what has been done in the past?

[Johan Commelin]

I'm not sure if we have a consistent guideline here. I personally think that a remark along the lines of "The additive analogues are developed using to_additive." suffices in the module docstring.

[Johan Commelin]

cc @Julian Külshammer

[Johan Commelin]

Should we have a poll?

[Julian Külshammer]

I personally don't care either way and would also be fine with a poll. If I remember correctly, I did it like that already for group_theory order_of_element.lean

[Yaël Dillies]

I don't think it matters much. An allusion to to_additive in the module docstring is fine, copying everything between the additive and multiplicative version is fine.