# Derivations #

This file defines derivation. A derivation D from the R-algebra A to the A-module M is an R-linear map that satisfy the Leibniz rule D (a * b) = a * D b + D a * b.

## Main results #

• Derivation: The type of R-derivations from A to M. This has an A-module structure.
• Derivation.llcomp: We may compose linear maps and derivations to obtain a derivation, and the composition is bilinear.

See RingTheory.Derivation.Lie for

• derivation.lie_algebra: The R-derivations from A to A form a lie algebra over R.

and RingTheory.Derivation.ToSquareZero for

• derivationToSquareZeroEquivLift: The R-derivations from A into a square-zero ideal I of B corresponds to the lifts A →ₐ[R] B of the map A →ₐ[R] B ⧸ I.

## Future project #

• Generalize derivations into bimodules.
structure Derivation (R : Type u_1) (A : Type u_2) (M : Type u_3) [] [] [] [Algebra R A] [Module A M] [Module R M] extends :
Type (max u_2 u_3)

D : Derivation R A M is an R-linear map from A to M that satisfies the leibniz equality. We also require that D 1 = 0. See Derivation.mk' for a constructor that deduces this assumption from the Leibniz rule when M is cancellative.

TODO: update this when bimodules are defined.

• toFun : AM
• map_add' : ∀ (x y : A), (self).toFun (x + y) = (self).toFun x + (self).toFun y
• map_smul' : ∀ (m : R) (x : A), (self).toFun (m x) = () m (self).toFun x
• map_one_eq_zero' : self 1 = 0
• leibniz' : ∀ (a b : A), self (a * b) = a self b + b self a
Instances For
theorem Derivation.map_one_eq_zero' {R : Type u_1} {A : Type u_2} {M : Type u_3} [] [] [] [Algebra R A] [Module A M] [Module R M] (self : Derivation R A M) :
self 1 = 0
theorem Derivation.leibniz' {R : Type u_1} {A : Type u_2} {M : Type u_3} [] [] [] [Algebra R A] [Module A M] [Module R M] (self : Derivation R A M) (a : A) (b : A) :
self (a * b) = a self b + b self a
instance Derivation.instFunLike {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] :
FunLike (Derivation R A M) A M
Equations
• Derivation.instFunLike = { coe := fun (D : Derivation R A M) => (D).toFun, coe_injective' := }
instance Derivation.instAddMonoidHomClass {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] :
Equations
• =
theorem Derivation.toFun_eq_coe {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] (D : Derivation R A M) :
(D).toFun = D
def Derivation.Simps.apply {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] (D : Derivation R A M) :
AM

See Note [custom simps projection]

Equations
Instances For
instance Derivation.hasCoeToLinearMap {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] :
Coe (Derivation R A M) (A →ₗ[R] M)
Equations
• Derivation.hasCoeToLinearMap = { coe := fun (D : Derivation R A M) => D }
@[simp]
theorem Derivation.mk_coe {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] (f : A →ₗ[R] M) (h₁ : f 1 = 0) (h₂ : ∀ (a b : A), f (a * b) = a f b + b f a) :
{ toLinearMap := f, map_one_eq_zero' := h₁, leibniz' := h₂ } = f
@[simp]
theorem Derivation.coeFn_coe {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] (f : Derivation R A M) :
f = f
theorem Derivation.coe_injective {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] :
Function.Injective DFunLike.coe
theorem Derivation.ext {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] {D1 : Derivation R A M} {D2 : Derivation R A M} (H : ∀ (a : A), D1 a = D2 a) :
D1 = D2
theorem Derivation.congr_fun {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] {D1 : Derivation R A M} {D2 : Derivation R A M} (h : D1 = D2) (a : A) :
D1 a = D2 a
theorem Derivation.map_add {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] (D : Derivation R A M) (a : A) (b : A) :
D (a + b) = D a + D b
theorem Derivation.map_zero {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] (D : Derivation R A M) :
D 0 = 0
@[simp]
theorem Derivation.map_smul {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] (D : Derivation R A M) (r : R) (a : A) :
D (r a) = r D a
@[simp]
theorem Derivation.leibniz {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] (D : Derivation R A M) (a : A) (b : A) :
D (a * b) = a D b + b D a
@[simp]
theorem Derivation.map_smul_of_tower {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] {S : Type u_5} [SMul S A] [SMul S M] [] (D : Derivation R A M) (r : S) (a : A) :
D (r a) = r D a
@[simp]
theorem Derivation.map_one_eq_zero {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] (D : Derivation R A M) :
D 1 = 0
@[simp]
theorem Derivation.map_algebraMap {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] (D : Derivation R A M) (r : R) :
D (() r) = 0
@[simp]
theorem Derivation.map_natCast {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] (D : Derivation R A M) (n : ) :
D n = 0
@[simp]
theorem Derivation.leibniz_pow {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] (D : Derivation R A M) (a : A) (n : ) :
D (a ^ n) = n a ^ (n - 1) D a
@[simp]
theorem Derivation.map_aeval {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] (D : Derivation R A M) (P : ) (x : A) :
D (() P) = () (Polynomial.derivative P) D x
theorem Derivation.eqOn_adjoin {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] {D1 : Derivation R A M} {D2 : Derivation R A M} {s : Set A} (h : Set.EqOn (D1) (D2) s) :
Set.EqOn D1 D2 ()
theorem Derivation.ext_of_adjoin_eq_top {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] {D1 : Derivation R A M} {D2 : Derivation R A M} (s : Set A) (hs : = ) (h : Set.EqOn (D1) (D2) s) :
D1 = D2

If adjoin of a set is the whole algebra, then any two derivations equal on this set are equal on the whole algebra.

instance Derivation.instZero {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] :
Equations
• Derivation.instZero = { zero := { toLinearMap := 0, map_one_eq_zero' := , leibniz' := } }
@[simp]
theorem Derivation.coe_zero {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] :
0 = 0
@[simp]
theorem Derivation.coe_zero_linearMap {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] :
0 = 0
theorem Derivation.zero_apply {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] (a : A) :
0 a = 0
instance Derivation.instAdd {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] :
Equations
• Derivation.instAdd = { add := fun (D1 D2 : Derivation R A M) => { toLinearMap := D1 + D2, map_one_eq_zero' := , leibniz' := } }
@[simp]
theorem Derivation.coe_add {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] (D1 : Derivation R A M) (D2 : Derivation R A M) :
(D1 + D2) = D1 + D2
@[simp]
theorem Derivation.coe_add_linearMap {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] (D1 : Derivation R A M) (D2 : Derivation R A M) :
(D1 + D2) = D1 + D2
theorem Derivation.add_apply {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] {D1 : Derivation R A M} {D2 : Derivation R A M} (a : A) :
(D1 + D2) a = D1 a + D2 a
instance Derivation.instInhabited {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] :
Equations
• Derivation.instInhabited = { default := 0 }
instance Derivation.instSMul {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] {S : Type u_5} [] [] [] [] :
SMul S (Derivation R A M)
Equations
• Derivation.instSMul = { smul := fun (r : S) (D : Derivation R A M) => { toLinearMap := r D, map_one_eq_zero' := , leibniz' := } }
@[simp]
theorem Derivation.coe_smul {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] {S : Type u_5} [] [] [] [] (r : S) (D : Derivation R A M) :
(r D) = r D
@[simp]
theorem Derivation.coe_smul_linearMap {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] {S : Type u_5} [] [] [] [] (r : S) (D : Derivation R A M) :
(r D) = r D
theorem Derivation.smul_apply {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] (a : A) {S : Type u_5} [] [] [] [] (r : S) (D : Derivation R A M) :
(r D) a = r D a
instance Derivation.instAddCommMonoid {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] :
Equations
def Derivation.coeFnAddMonoidHom {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] :
Derivation R A M →+ AM

coe_fn as an AddMonoidHom.

Equations
• Derivation.coeFnAddMonoidHom = { toFun := DFunLike.coe, map_zero' := , map_add' := }
Instances For
instance Derivation.instDistribMulAction {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] {S : Type u_5} [] [] [] [] :
Equations
instance Derivation.instIsCentralScalar {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] {S : Type u_5} [] [] [] [] [] [] :
Equations
• =
instance Derivation.instIsScalarTower {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] {S : Type u_5} {T : Type u_6} [] [] [] [] [] [] [] [] [SMul S T] [] :
Equations
• =
instance Derivation.instSMulCommClass {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] {S : Type u_5} {T : Type u_6} [] [] [] [] [] [] [] [] [] :
Equations
• =
instance Derivation.instModule {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] {S : Type u_5} [] [Module S M] [] [] :
Module S (Derivation R A M)
Equations
def LinearMap.compDer {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] {N : Type u_5} [] [Module A N] [Module R N] [] [] (f : M →ₗ[A] N) :

We can push forward derivations using linear maps, i.e., the composition of a derivation with a linear map is a derivation. Furthermore, this operation is linear on the spaces of derivations.

Equations
• f.compDer = { toFun := fun (D : Derivation R A M) => { toLinearMap := R f ∘ₗ D, map_one_eq_zero' := , leibniz' := }, map_add' := , map_smul' := }
Instances For
@[simp]
theorem Derivation.coe_to_linearMap_comp {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] (D : Derivation R A M) {N : Type u_5} [] [Module A N] [Module R N] [] [] (f : M →ₗ[A] N) :
(f.compDer D) = R f ∘ₗ D
@[simp]
theorem Derivation.coe_comp {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] (D : Derivation R A M) {N : Type u_5} [] [Module A N] [Module R N] [] [] (f : M →ₗ[A] N) :
(f.compDer D) = (R f ∘ₗ D)
@[simp]
theorem Derivation.llcomp_apply {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] {N : Type u_5} [] [Module A N] [Module R N] [] [] (f : M →ₗ[A] N) :
Derivation.llcomp f = f.compDer
def Derivation.llcomp {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] {N : Type u_5} [] [Module A N] [Module R N] [] [] :

The composition of a derivation with a linear map as a bilinear map

Equations
• Derivation.llcomp = { toFun := fun (f : M →ₗ[A] N) => f.compDer, map_add' := , map_smul' := }
Instances For
def LinearEquiv.compDer {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] {N : Type u_5} [] [Module A N] [Module R N] [] [] (e : M ≃ₗ[A] N) :

Pushing a derivation forward through a linear equivalence is an equivalence.

Equations
• e.compDer = let __src := (e).compDer; { toLinearMap := __src, invFun := (e.symm).compDer, left_inv := , right_inv := }
Instances For
@[simp]
theorem Derivation.linearEquiv_coe_to_linearMap_comp {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] (D : Derivation R A M) {N : Type u_5} [] [Module A N] [Module R N] [] [] (e : M ≃ₗ[A] N) :
(e.compDer D) = R e ∘ₗ D
@[simp]
theorem Derivation.linearEquiv_coe_comp {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] (D : Derivation R A M) {N : Type u_5} [] [Module A N] [Module R N] [] [] (e : M ≃ₗ[A] N) :
(e.compDer D) = (R e ∘ₗ D)
@[simp]
theorem Derivation.compAlgebraMap_apply {R : Type u_1} (A : Type u_2) {B : Type u_3} {M : Type u_4} [] [] [] [] [Algebra R A] [Algebra R B] [Module A M] [Module B M] [Module R M] [Algebra A B] [] [] (d : Derivation R B M) :
∀ (a : A), a = d (() a)
def Derivation.compAlgebraMap {R : Type u_1} (A : Type u_2) {B : Type u_3} {M : Type u_4} [] [] [] [] [Algebra R A] [Algebra R B] [Module A M] [Module B M] [Module R M] [Algebra A B] [] [] (d : Derivation R B M) :

For a tower R → A → B and an R-derivation B → M, we may compose with A → B to obtain an R-derivation A → M.

Equations
• = { toLinearMap := d ∘ₗ ().toLinearMap, map_one_eq_zero' := , leibniz' := }
Instances For
def Derivation.restrictScalars (R : Type u_1) {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] {S : Type u_5} [] [Algebra S A] [Module S M] [] (d : Derivation S A M) :

If A is both an R-algebra and an S-algebra; M is both an R-module and an S-module, then an S-derivation A → M is also an R-derivation if it is also R-linear.

Equations
• = { toLinearMap := R d, map_one_eq_zero' := , leibniz' := }
Instances For
theorem Derivation.coe_restrictScalars (R : Type u_1) {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] {S : Type u_5} [] [Algebra S A] [Module S M] [] (d : Derivation S A M) :
= d
@[simp]
theorem Derivation.restrictScalars_apply (R : Type u_1) {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] {S : Type u_5} [] [Algebra S A] [Module S M] [] (d : Derivation S A M) (x : A) :
x = d x
def Derivation.mk' {R : Type u_1} [] {A : Type u_2} [] [Algebra R A] {M : Type u_3} [Module R M] [Module A M] (D : A →ₗ[R] M) (h : ∀ (a b : A), D (a * b) = a D b + b D a) :

Define Derivation R A M from a linear map when M is cancellative by verifying the Leibniz rule.

Equations
• = { toLinearMap := D, map_one_eq_zero' := , leibniz' := h }
Instances For
@[simp]
theorem Derivation.coe_mk' {R : Type u_1} [] {A : Type u_2} [] [Algebra R A] {M : Type u_3} [Module R M] [Module A M] (D : A →ₗ[R] M) (h : ∀ (a b : A), D (a * b) = a D b + b D a) :
() = D
@[simp]
theorem Derivation.coe_mk'_linearMap {R : Type u_1} [] {A : Type u_2} [] [Algebra R A] {M : Type u_3} [Module R M] [Module A M] (D : A →ₗ[R] M) (h : ∀ (a b : A), D (a * b) = a D b + b D a) :
() = D
theorem Derivation.map_neg {R : Type u_1} [] {A : Type u_2} [] [Algebra R A] {M : Type u_3} [] [Module A M] [Module R M] (D : Derivation R A M) (a : A) :
D (-a) = -D a
theorem Derivation.map_sub {R : Type u_1} [] {A : Type u_2} [] [Algebra R A] {M : Type u_3} [] [Module A M] [Module R M] (D : Derivation R A M) (a : A) (b : A) :
D (a - b) = D a - D b
@[simp]
theorem Derivation.map_intCast {R : Type u_1} [] {A : Type u_2} [] [Algebra R A] {M : Type u_3} [] [Module A M] [Module R M] (D : Derivation R A M) (n : ) :
D n = 0
@[deprecated Derivation.map_natCast]
theorem Derivation.map_coe_nat {R : Type u_1} {A : Type u_2} {M : Type u_4} [] [] [] [Algebra R A] [Module A M] [Module R M] (D : Derivation R A M) (n : ) :
D n = 0

Alias of Derivation.map_natCast.

@[deprecated Derivation.map_intCast]
theorem Derivation.map_coe_int {R : Type u_1} [] {A : Type u_2} [] [Algebra R A] {M : Type u_3} [] [Module A M] [Module R M] (D : Derivation R A M) (n : ) :
D n = 0

Alias of Derivation.map_intCast.

theorem Derivation.leibniz_of_mul_eq_one {R : Type u_1} [] {A : Type u_2} [] [Algebra R A] {M : Type u_3} [] [Module A M] [Module R M] (D : Derivation R A M) {a : A} {b : A} (h : a * b = 1) :
D a = -a ^ 2 D b
theorem Derivation.leibniz_invOf {R : Type u_1} [] {A : Type u_2} [] [Algebra R A] {M : Type u_3} [] [Module A M] [Module R M] (D : Derivation R A M) (a : A) [] :
D a = -a ^ 2 D a
theorem Derivation.leibniz_inv {R : Type u_1} [] {M : Type u_3} [] [Module R M] {K : Type u_4} [] [Module K M] [Algebra R K] (D : Derivation R K M) (a : K) :
D a⁻¹ = -a⁻¹ ^ 2 D a
theorem Derivation.leibniz_div {R : Type u_1} [] {M : Type u_3} [] [Module R M] {K : Type u_4} [] [Module K M] [Algebra R K] (D : Derivation R K M) (a : K) (b : K) :
D (a / b) = b⁻¹ ^ 2 (b D a - a D b)
theorem Derivation.leibniz_div_const {R : Type u_1} [] {M : Type u_3} [] [Module R M] {K : Type u_4} [] [Module K M] [Algebra R K] (D : Derivation R K M) (a : K) (b : K) (h : D b = 0) :
D (a / b) = b⁻¹ D a
theorem Derivation.leibniz_zpow {R : Type u_1} [] {M : Type u_3} [] [Module R M] {K : Type u_4} [] [Module K M] [Algebra R K] (D : Derivation R K M) (a : K) (n : ) :
D (a ^ n) = n a ^ (n - 1) D a
instance Derivation.instNeg {R : Type u_1} [] {A : Type u_2} [] [Algebra R A] {M : Type u_3} [] [Module A M] [Module R M] :
Neg (Derivation R A M)
Equations
@[simp]
theorem Derivation.coe_neg {R : Type u_1} [] {A : Type u_2} [] [Algebra R A] {M : Type u_3} [] [Module A M] [Module R M] (D : Derivation R A M) :
(-D) = -D
@[simp]
theorem Derivation.coe_neg_linearMap {R : Type u_1} [] {A : Type u_2} [] [Algebra R A] {M : Type u_3} [] [Module A M] [Module R M] (D : Derivation R A M) :
(-D) = -D
theorem Derivation.neg_apply {R : Type u_1} [] {A : Type u_2} [] [Algebra R A] {M : Type u_3} [] [Module A M] [Module R M] (D : Derivation R A M) (a : A) :
(-D) a = -D a
instance Derivation.instSub {R : Type u_1} [] {A : Type u_2} [] [Algebra R A] {M : Type u_3} [] [Module A M] [Module R M] :
Sub (Derivation R A M)
Equations
@[simp]
theorem Derivation.coe_sub {R : Type u_1} [] {A : Type u_2} [] [Algebra R A] {M : Type u_3} [] [Module A M] [Module R M] (D1 : Derivation R A M) (D2 : Derivation R A M) :
(D1 - D2) = D1 - D2
@[simp]
theorem Derivation.coe_sub_linearMap {R : Type u_1} [] {A : Type u_2} [] [Algebra R A] {M : Type u_3} [] [Module A M] [Module R M] (D1 : Derivation R A M) (D2 : Derivation R A M) :
(D1 - D2) = D1 - D2
theorem Derivation.sub_apply {R : Type u_1} [] {A : Type u_2} [] [Algebra R A] {M : Type u_3} [] [Module A M] [Module R M] {D1 : Derivation R A M} {D2 : Derivation R A M} (a : A) :
(D1 - D2) a = D1 a - D2 a
instance Derivation.instAddCommGroup {R : Type u_1} [] {A : Type u_2} [] [Algebra R A] {M : Type u_3} [] [Module A M] [Module R M] :
Equations