## Stream: maths

### Topic: add_group to group

#### Kevin Buzzard (Jul 24 2020 at 19:01):

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 (Jul 24 2020 at 19:10):

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 (Jul 24 2020 at 19:11):

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

#### Yury G. Kudryashov (Jul 24 2020 at 19:54):

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

Last updated: May 14 2021 at 19:21 UTC