add_group to group

Stream: maths

[Kevin Buzzard]

I'm really surprised this works. It came up when refactoring subgroups:

import tactic

example (A : Type) [add_group A] (x : A) (m n : ℤ) :
gsmul (m+n) x = gsmul m x + gsmul n x := gpow_add x m n
/-
gpow_add : ∀ {G : Type} [_inst_1 : group G] (a : G) (m n : ℤ),
  a ^ (m + n) = a ^ m * a ^ n
-/

Lean has to infer G given x, and if it goes for G = A then it's not going to find the group instance because A is an add_group. But G=multiplicative A works. What makes Lean try that?

[Jalex Stark]

i'm not at my VSCode right now, but I think if there is an instance [add_group G] : group G := multiplicative G, then typeclass inference should just do it

[Jalex Stark]

(and of course for this to work we can only register multiplicative as an instance and not additive)

[Yury G. Kudryashov]

gsmul is defined as @gpow (multiplicative A) _ a n so Lean already has access to multiplicative A.