mathlib3 documentation

ring_theory.derivation.basic

Derivations #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

See ring_theory.derivation.lie for

and ring_theory.derivation.to_square_zero for

Future project #

source
structure derivation (R : Type u_1) (A : Type u_2) [comm_semiring R] [comm_semiring A] [algebra R A] (M : Type u_3) [add_comm_monoid M] [module A M] [module R M] :
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.

Instances for derivation
source
@[protected, instance]
def derivation.add_monoid_hom_class {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] :
add_monoid_hom_class (derivation R A M) A M
Equations
source
@[protected, instance]
def derivation.has_coe_to_fun {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] :
has_coe_to_fun (derivation R A M) (λ (_x : derivation R A M), A → M)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations
source
theorem derivation.to_fun_eq_coe {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] (D : derivation R A M) :
D.to_linear_map.to_fun = ⇑D
source
@[protected, instance]
def derivation.has_coe_to_linear_map {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] :
has_coe (derivation R A M) (A →ₗ[R] M)
Equations
source
@[simp]
theorem derivation.to_linear_map_eq_coe {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] (D : derivation R A M) :
D.to_linear_map = ↑D
source
@[simp]
theorem derivation.mk_coe {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [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) :
⇑{to_linear_map := f, map_one_eq_zero' := h₁, leibniz' := h₂} = ⇑f
source
@[simp, norm_cast]
theorem derivation.coe_fn_coe {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] (f : derivation R A M) :
⇑↑f = ⇑f
source
theorem derivation.coe_injective {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] :
function.injective coe_fn
source
@[ext]
theorem derivation.ext {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] {D1 D2 : derivation R A M} (H : ∀ (a : A), ⇑D1 a = ⇑D2 a) :
D1 = D2
source
theorem derivation.congr_fun {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] {D1 D2 : derivation R A M} (h : D1 = D2) (a : A) :
⇑D1 a = ⇑D2 a
source
@[protected]
theorem derivation.map_add {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] (D : derivation R A M) (a b : A) :
⇑D (a + b) = ⇑D a + ⇑D b
source
@[protected]
theorem derivation.map_zero {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] (D : derivation R A M) :
⇑D 0 = 0
source
@[simp]
theorem derivation.map_smul {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] (D : derivation R A M) (r : R) (a : A) :
⇑D (r • a) = r • ⇑D a
source
@[simp]
theorem derivation.leibniz {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] (D : derivation R A M) (a b : A) :
⇑D (a * b) = a • ⇑D b + b • ⇑D a
source
theorem derivation.map_sum {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] (D : derivation R A M) {ι : Type u_4} (s : finset ι) (f : ι → A) :
⇑D (s.sum (λ (i : ι), f i)) = s.sum (λ (i : ι), ⇑D (f i))
source
@[simp]
theorem derivation.map_smul_of_tower {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] {S : Type u_4} [has_smul S A] [has_smul S M] [linear_map.compatible_smul A M S R] (D : derivation R A M) (r : S) (a : A) :
⇑D (r • a) = r • ⇑D a
source
@[simp]
theorem derivation.map_one_eq_zero {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] (D : derivation R A M) :
⇑D 1 = 0
source
@[simp]
theorem derivation.map_algebra_map {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] (D : derivation R A M) (r : R) :
⇑D (⇑(algebra_map R A) r) = 0
source
@[simp]
theorem derivation.map_coe_nat {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] (D : derivation R A M) (n : ℕ) :
⇑D ↑n = 0
source
@[simp]
theorem derivation.leibniz_pow {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] (D : derivation R A M) (a : A) (n : ℕ) :
⇑D (a ^ n) = n • a ^ (n - 1) • ⇑D a
source
theorem derivation.eq_on_adjoin {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] {D1 D2 : derivation R A M} {s : set A} (h : set.eq_on ⇑D1 ⇑D2 s) :
set.eq_on ⇑D1 ⇑D2 ↑(algebra.adjoin R s)
source
theorem derivation.ext_of_adjoin_eq_top {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] {D1 D2 : derivation R A M} (s : set A) (hs : algebra.adjoin R s = ⊤) (h : set.eq_on ⇑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.

source
@[protected, instance]
def derivation.has_zero {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] :
has_zero (derivation R A M)
Equations
source
@[simp]
theorem derivation.coe_zero {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] :
⇑0 = 0
source
@[simp]
theorem derivation.coe_zero_linear_map {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] :
↑0 = 0
source
theorem derivation.zero_apply {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] (a : A) :
⇑0 a = 0
source
@[protected, instance]
def derivation.has_add {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] :
has_add (derivation R A M)
Equations
source
@[simp]
theorem derivation.coe_add {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] (D1 D2 : derivation R A M) :
⇑(D1 + D2) = ⇑D1 + ⇑D2
source
@[simp]
theorem derivation.coe_add_linear_map {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] (D1 D2 : derivation R A M) :
↑(D1 + D2) = ↑D1 + ↑D2
source
theorem derivation.add_apply {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] {D1 D2 : derivation R A M} (a : A) :
⇑(D1 + D2) a = ⇑D1 a + ⇑D2 a
source
@[protected, instance]
def derivation.inhabited {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] :
inhabited (derivation R A M)
Equations
source
@[protected, instance]
def derivation.has_smul {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] {S : Type u_4} [monoid S] [distrib_mul_action S M] [smul_comm_class R S M] [smul_comm_class S A M] :
has_smul S (derivation R A M)
Equations
source
@[simp]
theorem derivation.coe_smul {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] {S : Type u_4} [monoid S] [distrib_mul_action S M] [smul_comm_class R S M] [smul_comm_class S A M] (r : S) (D : derivation R A M) :
⇑(r • D) = r • ⇑D
source
@[simp]
theorem derivation.coe_smul_linear_map {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] {S : Type u_4} [monoid S] [distrib_mul_action S M] [smul_comm_class R S M] [smul_comm_class S A M] (r : S) (D : derivation R A M) :
↑(r • D) = r • ↑D
source
theorem derivation.smul_apply {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] (a : A) {S : Type u_4} [monoid S] [distrib_mul_action S M] [smul_comm_class R S M] [smul_comm_class S A M] (r : S) (D : derivation R A M) :
⇑(r • D) a = r • ⇑D a
source
@[protected, instance]
def derivation.add_comm_monoid {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] :
add_comm_monoid (derivation R A M)
Equations
source
def derivation.coe_fn_add_monoid_hom {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] :
derivation R A M →+ A → M

coe_fn as an add_monoid_hom.

Equations
source
@[protected, instance]
def derivation.distrib_mul_action {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] {S : Type u_4} [monoid S] [distrib_mul_action S M] [smul_comm_class R S M] [smul_comm_class S A M] :
distrib_mul_action S (derivation R A M)
Equations
source
@[protected, instance]
def derivation.is_central_scalar {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] {S : Type u_4} [monoid S] [distrib_mul_action S M] [smul_comm_class R S M] [smul_comm_class S A M] [distrib_mul_action Sᵐᵒᵖ M] [is_central_scalar S M] :
is_central_scalar S (derivation R A M)
source
@[protected, instance]
def derivation.is_scalar_tower {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] {S : Type u_4} {T : Type u_5} [monoid S] [distrib_mul_action S M] [smul_comm_class R S M] [smul_comm_class S A M] [monoid T] [distrib_mul_action T M] [smul_comm_class R T M] [smul_comm_class T A M] [has_smul S T] [is_scalar_tower S T M] :
is_scalar_tower S T (derivation R A M)
source
@[protected, instance]
def derivation.smul_comm_class {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] {S : Type u_4} {T : Type u_5} [monoid S] [distrib_mul_action S M] [smul_comm_class R S M] [smul_comm_class S A M] [monoid T] [distrib_mul_action T M] [smul_comm_class R T M] [smul_comm_class T A M] [smul_comm_class S T M] :
smul_comm_class S T (derivation R A M)
source
@[protected, instance]
def derivation.module {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] {S : Type u_4} [semiring S] [module S M] [smul_comm_class R S M] [smul_comm_class S A M] :
module S (derivation R A M)
Equations
source
def linear_map.comp_der {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] {N : Type u_4} [add_comm_monoid N] [module A N] [module R N] [is_scalar_tower R A M] [is_scalar_tower R A N] (f : M →ₗ[A] N) :
derivation R A M →ₗ[R] derivation R 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
source
@[simp]
theorem derivation.coe_to_linear_map_comp {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] (D : derivation R A M) {N : Type u_4} [add_comm_monoid N] [module A N] [module R N] [is_scalar_tower R A M] [is_scalar_tower R A N] (f : M →ₗ[A] N) :
↑(⇑(f.comp_der) D) = ↑f.comp ↑D
source
@[simp]
theorem derivation.coe_comp {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] (D : derivation R A M) {N : Type u_4} [add_comm_monoid N] [module A N] [module R N] [is_scalar_tower R A M] [is_scalar_tower R A N] (f : M →ₗ[A] N) :
⇑(⇑(f.comp_der) D) = ⇑(↑f.comp ↑D)
source
def derivation.llcomp {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] {N : Type u_4} [add_comm_monoid N] [module A N] [module R N] [is_scalar_tower R A M] [is_scalar_tower R A N] :
(M →ₗ[A] N) →ₗ[A] derivation R A M →ₗ[R] derivation R A N

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

Equations
source
@[simp]
theorem derivation.llcomp_apply {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] {N : Type u_4} [add_comm_monoid N] [module A N] [module R N] [is_scalar_tower R A M] [is_scalar_tower R A N] (f : M →ₗ[A] N) :
⇑derivation.llcomp f = f.comp_der
source
def linear_equiv.comp_der {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] {N : Type u_4} [add_comm_monoid N] [module A N] [module R N] [is_scalar_tower R A M] [is_scalar_tower R A N] (e : M ≃ₗ[A] N) :
derivation R A M ≃ₗ[R] derivation R A N

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

Equations
source
@[protected]
def derivation.restrict_scalars (R : Type u_1) [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_comm_monoid M] [module A M] [module R M] {S : Type u_4} [comm_semiring S] [algebra S A] [module S M] [linear_map.compatible_smul A M R S] (d : derivation S A M) :
derivation R 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
source
def derivation.mk' {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_cancel_comm_monoid M] [module R M] [module A M] (D : A →ₗ[R] M) (h : ∀ (a b : A), ⇑D (a * b) = a • ⇑D b + b • ⇑D a) :
derivation R A M

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

Equations
source
@[simp]
theorem derivation.coe_mk' {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_cancel_comm_monoid M] [module R M] [module A M] (D : A →ₗ[R] M) (h : ∀ (a b : A), ⇑D (a * b) = a • ⇑D b + b • ⇑D a) :
⇑(derivation.mk' D h) = ⇑D
source
@[simp]
theorem derivation.coe_mk'_linear_map {R : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] {M : Type u_3} [add_cancel_comm_monoid M] [module R M] [module A M] (D : A →ₗ[R] M) (h : ∀ (a b : A), ⇑D (a * b) = a • ⇑D b + b • ⇑D a) :
↑(derivation.mk' D h) = D
source
@[protected]
theorem derivation.map_neg {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [algebra R A] {M : Type u_3} [add_comm_group M] [module A M] [module R M] (D : derivation R A M) (a : A) :
⇑D (-a) = -⇑D a
source
@[protected]
theorem derivation.map_sub {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [algebra R A] {M : Type u_3} [add_comm_group M] [module A M] [module R M] (D : derivation R A M) (a b : A) :
⇑D (a - b) = ⇑D a - ⇑D b
source
@[simp]
theorem derivation.map_coe_int {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [algebra R A] {M : Type u_3} [add_comm_group M] [module A M] [module R M] (D : derivation R A M) (n : ℤ) :
⇑D ↑n = 0
source
theorem derivation.leibniz_of_mul_eq_one {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [algebra R A] {M : Type u_3} [add_comm_group M] [module A M] [module R M] (D : derivation R A M) {a b : A} (h : a * b = 1) :
⇑D a = -a ^ 2 • ⇑D b
source
theorem derivation.leibniz_inv_of {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [algebra R A] {M : Type u_3} [add_comm_group M] [module A M] [module R M] (D : derivation R A M) (a : A) [invertible a] :
⇑D (⅟ a) = -⅟ a ^ 2 • ⇑D a
source
theorem derivation.leibniz_inv {R : Type u_1} [comm_ring R] {M : Type u_3} [add_comm_group M] [module R M] {K : Type u_2} [field K] [module K M] [algebra R K] (D : derivation R K M) (a : K) :
⇑D a⁻¹ = -a⁻¹ ^ 2 • ⇑D a
source
@[protected, instance]
def derivation.has_neg {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [algebra R A] {M : Type u_3} [add_comm_group M] [module A M] [module R M] :
has_neg (derivation R A M)
Equations
source
@[simp]
theorem derivation.coe_neg {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [algebra R A] {M : Type u_3} [add_comm_group M] [module A M] [module R M] (D : derivation R A M) :
⇑-D = -⇑D
source
@[simp]
theorem derivation.coe_neg_linear_map {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [algebra R A] {M : Type u_3} [add_comm_group M] [module A M] [module R M] (D : derivation R A M) :
↑-D = -↑D
source
theorem derivation.neg_apply {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [algebra R A] {M : Type u_3} [add_comm_group M] [module A M] [module R M] (D : derivation R A M) (a : A) :
(⇑-D) a = -⇑D a
source
@[protected, instance]
def derivation.has_sub {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [algebra R A] {M : Type u_3} [add_comm_group M] [module A M] [module R M] :
has_sub (derivation R A M)
Equations
source
@[simp]
theorem derivation.coe_sub {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [algebra R A] {M : Type u_3} [add_comm_group M] [module A M] [module R M] (D1 D2 : derivation R A M) :
⇑(D1 - D2) = ⇑D1 - ⇑D2
source
@[simp]
theorem derivation.coe_sub_linear_map {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [algebra R A] {M : Type u_3} [add_comm_group M] [module A M] [module R M] (D1 D2 : derivation R A M) :
↑(D1 - D2) = ↑D1 - ↑D2
source
theorem derivation.sub_apply {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [algebra R A] {M : Type u_3} [add_comm_group M] [module A M] [module R M] {D1 D2 : derivation R A M} (a : A) :
⇑(D1 - D2) a = ⇑D1 a - ⇑D2 a
source
@[protected, instance]
def derivation.add_comm_group {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [algebra R A] {M : Type u_3} [add_comm_group M] [module A M] [module R M] :
add_comm_group (derivation R A M)
Equations