to_additive and structure

Stream: mathlib4

[Christopher Hoskin]

If I try:

import Mathlib.Tactic.ToAdditive

universe u

@[to_additive]
structure IsMulCentral {M : Type u} [Mul M] (z : M) : Prop where
  comm (a : M) : z * a = a * z
  left_assoc (b c : M) : z * (b * c) = (z * b) * c
  mid_assoc (a c : M) : (a * z) * c = a * (z * c)
  right_assoc (a b : M) : (a * b) * z = a * (b * z)

Then the to_additive gives me the error Expected IsAddCentral to have a value.

There appear to be other examples of using to_additive with a structure in Mathlib e.g. https://github.com/leanprover-community/mathlib4/blob/a063f8c5f58507dfc51a551d0d47ae5fb83082aa/Mathlib/MeasureTheory/Group/FundamentalDomain.lean#L60 - so why can't I get this one to work?

Thanks,

Christopher

[Damiano Testa]

I think that you should declare the additive structure before, and then the to_additive tag links the two.

[Damiano Testa]

Note that docs#MeasureTheory.IsFundamentalDomain is in the source, it is not autogenerated.

https://github.com/leanprover-community/mathlib4/blob/e8477a93d0167f0ba267556bd90720efe762529c/Mathlib/MeasureTheory/Group/FundamentalDomain.lean#L50C11-L50C33

[Damiano Testa]

to_additive should start to do its magic on lemmas, where it will know to replace IsMulCentral with whatever you want it to align (and to_additive suspects that it will be IsAddCentral).

[Floris van Doorn]

@[to_additive] doesn't auto-generate structures yet (it will be able to do this, this just hasn't been programmed yet). So you have to write the additive version first, as Damiano said.