Group instances for FunLike types

In this file we define various instances related to groups for FunLike types.

For example given a FunLike F α β with IsMulApply F α β and Semigroup β, then F is naturally a semigroup. Note that currently, these are not registered as instances, but only abbrevs to avoid long typeclass searches.

Moreover, we define the homomorphism FunLike.coeMulHom : F →* α → β that acts by coercion. This definition is mainly needed to define a module instance on F.

def FunLike.coeMulHom (F : Type u_1) (α : Type u_2) (β : Type u_3) [FunLike F α β] [Mul F] [Mul β] [IsMulApply F α β] : F →ₙ* α → β

Coercion as a multiplicative homomorphism.

def FunLike.coeAddHom (F : Type u_1) (α : Type u_2) (β : Type u_3) [FunLike F α β] [Add F] [Add β] [IsAddApply F α β] : F →ₙ+ α → β

Coercion as an additive homomorphism.

@[simp]

theorem FunLike.coeMulHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Mul F] [Mul β] [IsMulApply F α β] (f : F) : (coeMulHom F α β) f = ⇑f

@[simp]

theorem FunLike.coeAddHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Add F] [Add β] [IsAddApply F α β] (f : F) : (coeAddHom F α β) f = ⇑f

theorem FunLike.coe_coeMulHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Mul F] [Mul β] [IsMulApply F α β] : ⇑(coeMulHom F α β) = DFunLike.coe

theorem FunLike.coe_coeAddHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Add F] [Add β] [IsAddApply F α β] : ⇑(coeAddHom F α β) = DFunLike.coe

theorem FunLike.coeMulHom_injective {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Mul F] [Mul β] [IsMulApply F α β] : Function.Injective ⇑(coeMulHom F α β)

theorem FunLike.coeAddHom_injective {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Add F] [Add β] [IsAddApply F α β] : Function.Injective ⇑(coeAddHom F α β)

def FunLike.coeMonoidHom (F : Type u_1) (α : Type u_2) (β : Type u_3) [FunLike F α β] [MulOne F] [MulOneClass β] [IsOneApply F α β] [IsMulApply F α β] : F →* α → β

Coercion as a monoid homomorphism.

def FunLike.coeAddMonoidHom (F : Type u_1) (α : Type u_2) (β : Type u_3) [FunLike F α β] [AddZero F] [AddZeroClass β] [IsZeroApply F α β] [IsAddApply F α β] : F →+ α → β

Coercion as an additive monoid homomorphism.

@[simp]

theorem FunLike.coeMonoidHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [MulOne F] [MulOneClass β] [IsOneApply F α β] [IsMulApply F α β] (f : F) : (coeMonoidHom F α β) f = ⇑f

@[simp]

theorem FunLike.coeAddMonoidHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [AddZero F] [AddZeroClass β] [IsZeroApply F α β] [IsAddApply F α β] (f : F) : (coeAddMonoidHom F α β) f = ⇑f

theorem FunLike.coe_coeMonoidHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [MulOne F] [MulOneClass β] [IsOneApply F α β] [IsMulApply F α β] : ⇑(coeMonoidHom F α β) = DFunLike.coe

theorem FunLike.coe_coeAddMonoidHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [AddZero F] [AddZeroClass β] [IsZeroApply F α β] [IsAddApply F α β] : ⇑(coeAddMonoidHom F α β) = DFunLike.coe

theorem FunLike.coe_coeMonoidHom' {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [MulOne F] [MulOneClass β] [IsOneApply F α β] [IsMulApply F α β] : ↑(coeMonoidHom F α β) = coeMulHom F α β

theorem FunLike.coe_coeAddMonoidHom' {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [AddZero F] [AddZeroClass β] [IsZeroApply F α β] [IsAddApply F α β] : ↑(coeAddMonoidHom F α β) = coeAddHom F α β

theorem FunLike.coeMonoidHom_injective {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [MulOne F] [MulOneClass β] [IsOneApply F α β] [IsMulApply F α β] : Function.Injective ⇑(coeMonoidHom F α β)

theorem FunLike.coeAddMonoidHom_injective {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [AddZero F] [AddZeroClass β] [IsZeroApply F α β] [IsAddApply F α β] : Function.Injective ⇑(coeAddMonoidHom F α β)

@[reducible, inline]

abbrev FunLike.semigroup {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Mul F] [Semigroup β] [IsMulApply F α β] : Semigroup F

A FunLike type that satisfies (f * g) x = f x * g x is a semigroup if β is a semigroup.

@[reducible, inline]

abbrev FunLike.addSemigroup {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Add F] [AddSemigroup β] [IsAddApply F α β] : AddSemigroup F

A FunLike type that satisfies (f + g) x = f x + g x is an additive semigroup if β is an additive semigroup.

@[reducible, inline]

abbrev FunLike.commSemigroup {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Mul F] [CommSemigroup β] [IsMulApply F α β] : CommSemigroup F

A FunLike type that satisfies (f * g) x = f x * g x is a commutative semigroup if β is a commutative semigroup.

@[reducible, inline]

abbrev FunLike.addCommSemigroup {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Add F] [AddCommSemigroup β] [IsAddApply F α β] : AddCommSemigroup F

A FunLike type that satisfies (f + g) x = f x + g x is a commatative additive semigroup if β is a commatative additive semigroup.

theorem FunLike.isLeftCancelMul {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Mul F] [Mul β] [IsLeftCancelMul β] [IsMulApply F α β] : IsLeftCancelMul F

A FunLike type that satisfies (f * g) x = f x * g x has left cancellative multiplication if β has left cancellative multiplication.

theorem FunLike.isLeftCancelAdd {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Add F] [Add β] [IsLeftCancelAdd β] [IsAddApply F α β] : IsLeftCancelAdd F

A FunLike type that satisfies (f + g) x = f x + g x has left cancellative addition if β has left cancellative addition.

theorem FunLike.isRightCancelMul {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Mul F] [Mul β] [IsRightCancelMul β] [IsMulApply F α β] : IsRightCancelMul F

A FunLike type that satisfies (f * g) x = f x * g x has right cancellative multiplication if β has right cancellative multiplication.

theorem FunLike.isRightCancelAdd {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Add F] [Add β] [IsRightCancelAdd β] [IsAddApply F α β] : IsRightCancelAdd F

A FunLike type that satisfies (f + g) x = f x + g x has right cancellative addition if β has right cancellative addition.

theorem FunLike.isCancelMul {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Mul F] [Mul β] [IsCancelMul β] [IsMulApply F α β] : IsCancelMul F

A FunLike type that satisfies (f * g) x = f x * g x has right multiplication if β has right multiplication.

theorem FunLike.isCancelAdd {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Add F] [Add β] [IsCancelAdd β] [IsAddApply F α β] : IsCancelAdd F

A FunLike type that satisfies (f + g) x = f x + g x has right addition if β has cancellative addition.

@[reducible, inline]

abbrev FunLike.leftCancelSemigroup {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Mul F] [LeftCancelSemigroup β] [IsMulApply F α β] : LeftCancelSemigroup F

A FunLike type that satisfies (f * g) x = f x * g x is a left cancel semigroup if β is a left cancel semigroup.

@[reducible, inline]

abbrev FunLike.addLeftCancelSemigroup {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Add F] [AddLeftCancelSemigroup β] [IsAddApply F α β] : AddLeftCancelSemigroup F

A FunLike type that satisfies (f + g) x = f x + g x is a left cancel additive semigroup if β is a left cancel additive semigroup.

@[reducible, inline]

abbrev FunLike.rightCancelSemigroup {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Mul F] [RightCancelSemigroup β] [IsMulApply F α β] : RightCancelSemigroup F

A FunLike type that satisfies (f * g) x = f x * g x is a right cancel semigroup if β is a right cancel semigroup.

@[reducible, inline]

abbrev FunLike.addRightCancelSemigroup {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Add F] [AddRightCancelSemigroup β] [IsAddApply F α β] : AddRightCancelSemigroup F

A FunLike type that satisfies (f + g) x = f x + g x is a right cancel additive semigroup if β is a right cancel additive semigroup.

@[reducible, inline]

abbrev FunLike.mulOneClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Mul F] [One F] [MulOneClass β] [IsOneApply F α β] [IsMulApply F α β] : MulOneClass F

A FunLike type with 1 and * is MulOneClass if β is a MulOneClass.

@[reducible, inline]

abbrev FunLike.addZeroClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Add F] [Zero F] [AddZeroClass β] [IsZeroApply F α β] [IsAddApply F α β] : AddZeroClass F

A FunLike type with 0 and + is AddZeroClass if β is a AddZeroClass.

@[reducible, inline]

abbrev FunLike.monoid {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Mul F] [One F] [Pow F ℕ] [Monoid β] [IsOneApply F α β] [IsMulApply F α β] [IsPowApply ℕ F α β] : Monoid F

A FunLike type that satisfies (f * g) x = f x * g x, 1 x = 1, and (f ^ n) x = f x ^ n is a monoid if β is a monoid.

@[reducible, inline]

abbrev FunLike.addMonoid {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Add F] [Zero F] [SMul ℕ F] [AddMonoid β] [IsZeroApply F α β] [IsAddApply F α β] [IsSMulApply ℕ F α β] : AddMonoid F

A FunLike type that satisfies (f + g) x = f x + g x, 0 x = 0, and (n • f) x = n • f x is an additive monoid if β is an additive monoid.

@[reducible, inline]

abbrev FunLike.leftCancelMonoid {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Mul F] [One F] [Pow F ℕ] [LeftCancelMonoid β] [IsOneApply F α β] [IsMulApply F α β] [IsPowApply ℕ F α β] : LeftCancelMonoid F

A FunLike type that satisfies (f * g) x = f x * g x, 1 x = 1, and (f ^ n) x = f x ^ n is a left cancel monoid if β is a left cancel monoid.

@[reducible, inline]

abbrev FunLike.addLeftCancelMonoid {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Add F] [Zero F] [SMul ℕ F] [AddLeftCancelMonoid β] [IsZeroApply F α β] [IsAddApply F α β] [IsSMulApply ℕ F α β] : AddLeftCancelMonoid F

A FunLike type that satisfies (f + g) x = f x + g x, 0 x = 0, and (n • f) x = n • f x is a left cancel additive monoid if β is a left cancel additive monoid.

@[reducible, inline]

abbrev FunLike.rightCancelMonoid {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Mul F] [One F] [Pow F ℕ] [RightCancelMonoid β] [IsOneApply F α β] [IsMulApply F α β] [IsPowApply ℕ F α β] : RightCancelMonoid F

A FunLike type that satisfies (f * g) x = f x * g x, 1 x = 1, and (f ^ n) x = f x ^ n is a right cancel monoid if β is a right cancel monoid.

@[reducible, inline]

abbrev FunLike.addRightCancelMonoid {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Add F] [Zero F] [SMul ℕ F] [AddRightCancelMonoid β] [IsZeroApply F α β] [IsAddApply F α β] [IsSMulApply ℕ F α β] : AddRightCancelMonoid F

A FunLike type that satisfies (f + g) x = f x + g x, 0 x = 0, and (n • f) x = n • f x is a right cancel additive monoid if β is a right cancel additive monoid.

@[reducible, inline]

abbrev FunLike.cancelMonoid {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Mul F] [One F] [Pow F ℕ] [CancelMonoid β] [IsOneApply F α β] [IsMulApply F α β] [IsPowApply ℕ F α β] : CancelMonoid F

A FunLike type that satisfies (f * g) x = f x * g x, 1 x = 1, and (f ^ n) x = f x ^ n is a cancel monoid if β is a cancel monoid.

@[reducible, inline]

abbrev FunLike.addCancelMonoid {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Add F] [Zero F] [SMul ℕ F] [AddCancelMonoid β] [IsZeroApply F α β] [IsAddApply F α β] [IsSMulApply ℕ F α β] : AddCancelMonoid F

A FunLike type that satisfies (f + g) x = f x + g x, 0 x = 0, and (n • f) x = n • f x is a cancel additive monoid if β is a cancel additive monoid.

@[reducible, inline]

abbrev FunLike.commMonoid {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Mul F] [One F] [Pow F ℕ] [CommMonoid β] [IsOneApply F α β] [IsMulApply F α β] [IsPowApply ℕ F α β] : CommMonoid F

A FunLike type that satisfies (f * g) x = f x * g x, 1 x = 1, and (f ^ n) x = f x ^ n is a commutative monoid if β is a commutative monoid.

@[reducible, inline]

abbrev FunLike.addCommMonoid {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Add F] [Zero F] [SMul ℕ F] [AddCommMonoid β] [IsZeroApply F α β] [IsAddApply F α β] [IsSMulApply ℕ F α β] : AddCommMonoid F

A FunLike type that satisfies (f + g) x = f x + g x, 0 x = 0, and (n • f) x = n • f x is a commutative additive monoid if β is a commutative additive monoid.

@[reducible, inline]

abbrev FunLike.cancelCommMonoid {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Mul F] [One F] [Pow F ℕ] [CancelCommMonoid β] [IsOneApply F α β] [IsMulApply F α β] [IsPowApply ℕ F α β] : CancelCommMonoid F

A FunLike type that satisfies (f * g) x = f x * g x, 1 x = 1, and (f ^ n) x = f x ^ n is a cancel commutative monoid if β is a cancel commutative monoid.

@[reducible, inline]

abbrev FunLike.addCancelCommMonoid {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Add F] [Zero F] [SMul ℕ F] [AddCancelCommMonoid β] [IsZeroApply F α β] [IsAddApply F α β] [IsSMulApply ℕ F α β] : AddCancelCommMonoid F

A FunLike type that satisfies (f + g) x = f x + g x, 0 x = 0, and (n • f) x = n • f x is a cancel commutative additive monoid if β is a cancel commutative additive monoid.

@[reducible, inline]

abbrev FunLike.involutiveInv {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Inv F] [InvolutiveInv β] [IsInvApply F α β] : InvolutiveInv F

A FunLike type with inverse that satisfies (f⁻¹) x = (f x)⁻¹ is an involutive inversion if β is an involutive inversion.

@[reducible, inline]

abbrev FunLike.involutiveNeg {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Neg F] [InvolutiveNeg β] [IsNegApply F α β] : InvolutiveNeg F

A FunLike type with negation that satisfies (- f) x = - (f x) is an involutive negation if β is an involutive negation.

@[reducible, inline]

abbrev FunLike.invOneClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [One F] [Inv F] [InvOneClass β] [IsOneApply F α β] [IsInvApply F α β] : InvOneClass F

A FunLike type with 1 and inverse is an InvOneClass if β is an InvOneClass.

@[reducible, inline]

abbrev FunLike.negZeroClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Zero F] [Neg F] [NegZeroClass β] [IsZeroApply F α β] [IsNegApply F α β] : NegZeroClass F

A FunLike type with 0 and negation is a NegZeroClass if β is a NegZeroClass.

@[reducible, inline]

abbrev FunLike.divInvMonoid {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Mul F] [One F] [Pow F ℕ] [Inv F] [Div F] [Pow F ℤ] [DivInvMonoid β] [IsOneApply F α β] [IsMulApply F α β] [IsInvApply F α β] [IsDivApply F α β] [IsPowApply ℕ F α β] [IsPowApply ℤ F α β] : DivInvMonoid F

A FunLike type is a DivInvMonoid if β is a DivInvMonoid.

@[reducible, inline]

abbrev FunLike.subNegMonoid {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Add F] [Zero F] [SMul ℕ F] [Neg F] [Sub F] [SMul ℤ F] [SubNegMonoid β] [IsZeroApply F α β] [IsAddApply F α β] [IsNegApply F α β] [IsSubApply F α β] [IsSMulApply ℕ F α β] [IsSMulApply ℤ F α β] : SubNegMonoid F

A FunLike type is a SubNegMonoid if β is a SubNegMonoid.

@[reducible, inline]

abbrev FunLike.divInvOneMonoid {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Mul F] [One F] [Pow F ℕ] [Inv F] [Div F] [Pow F ℤ] [DivInvOneMonoid β] [IsOneApply F α β] [IsMulApply F α β] [IsInvApply F α β] [IsDivApply F α β] [IsPowApply ℕ F α β] [IsPowApply ℤ F α β] : DivInvOneMonoid F

A FunLike type is a DivInvOneMonoid if β is a DivInvOneMonoid.

@[reducible, inline]

abbrev FunLike.subNegZeroMonoid {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Add F] [Zero F] [SMul ℕ F] [Neg F] [Sub F] [SMul ℤ F] [SubNegZeroMonoid β] [IsZeroApply F α β] [IsAddApply F α β] [IsNegApply F α β] [IsSubApply F α β] [IsSMulApply ℕ F α β] [IsSMulApply ℤ F α β] : SubNegZeroMonoid F

A FunLike type is a SubNegOneMonoid if β is a SubNegOneMonoid.

@[reducible, inline]

abbrev FunLike.divisionMonoid {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Mul F] [One F] [Pow F ℕ] [Inv F] [Div F] [Pow F ℤ] [DivisionMonoid β] [IsOneApply F α β] [IsMulApply F α β] [IsInvApply F α β] [IsDivApply F α β] [IsPowApply ℕ F α β] [IsPowApply ℤ F α β] : DivisionMonoid F

A FunLike type is a division monoid if β is a division monoid.

@[reducible, inline]

abbrev FunLike.subtractionMonoid {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Add F] [Zero F] [SMul ℕ F] [Neg F] [Sub F] [SMul ℤ F] [SubtractionMonoid β] [IsZeroApply F α β] [IsAddApply F α β] [IsNegApply F α β] [IsSubApply F α β] [IsSMulApply ℕ F α β] [IsSMulApply ℤ F α β] : SubtractionMonoid F

A FunLike type is a subtraction monoid if β is a subtraction monoid.

@[reducible, inline]

abbrev FunLike.divisionCommMonoid {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Mul F] [One F] [Pow F ℕ] [Inv F] [Div F] [Pow F ℤ] [DivisionCommMonoid β] [IsOneApply F α β] [IsMulApply F α β] [IsInvApply F α β] [IsDivApply F α β] [IsPowApply ℕ F α β] [IsPowApply ℤ F α β] : DivisionCommMonoid F

A FunLike type is a division commutative monoid if β is a division commutative monoid.

@[reducible, inline]

abbrev FunLike.subtractionCommMonoid {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Add F] [Zero F] [SMul ℕ F] [Neg F] [Sub F] [SMul ℤ F] [SubtractionCommMonoid β] [IsZeroApply F α β] [IsAddApply F α β] [IsNegApply F α β] [IsSubApply F α β] [IsSMulApply ℕ F α β] [IsSMulApply ℤ F α β] : SubtractionCommMonoid F

A FunLike type is a subtraction commutative monoid if β is a subtraction commutative monoid.

@[reducible, inline]

abbrev FunLike.group {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Mul F] [One F] [Pow F ℕ] [Inv F] [Div F] [Pow F ℤ] [Group β] [IsOneApply F α β] [IsMulApply F α β] [IsInvApply F α β] [IsDivApply F α β] [IsPowApply ℕ F α β] [IsPowApply ℤ F α β] : Group F

A FunLike type is a group if β is a group.

@[reducible, inline]

abbrev FunLike.addGroup {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Add F] [Zero F] [SMul ℕ F] [Neg F] [Sub F] [SMul ℤ F] [AddGroup β] [IsZeroApply F α β] [IsAddApply F α β] [IsNegApply F α β] [IsSubApply F α β] [IsSMulApply ℕ F α β] [IsSMulApply ℤ F α β] : AddGroup F

A FunLike type is an additive group if β is an additive group.

@[reducible, inline]

abbrev FunLike.commGroup {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Mul F] [One F] [Pow F ℕ] [Inv F] [Div F] [Pow F ℤ] [CommGroup β] [IsOneApply F α β] [IsMulApply F α β] [IsInvApply F α β] [IsDivApply F α β] [IsPowApply ℕ F α β] [IsPowApply ℤ F α β] : CommGroup F

A FunLike type is a commutative group if β is a commutative group.

@[reducible, inline]

abbrev FunLike.addCommGroup {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Add F] [Zero F] [SMul ℕ F] [Neg F] [Sub F] [SMul ℤ F] [AddCommGroup β] [IsZeroApply F α β] [IsAddApply F α β] [IsNegApply F α β] [IsSubApply F α β] [IsSMulApply ℕ F α β] [IsSMulApply ℤ F α β] : AddCommGroup F

A FunLike type is an additive commutative group if β is an additive commutative group.