Theorems · Inductive type · commutative algebra

Derivation

(R : Type u_1) →
  (A : Type u_2) →
    (M : Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : AddCommMonoid M] → [Algebra R A] → [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.

Defined in

Mathlib.RingTheory.Derivation.Basic

Cited by

293 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 7 definitions · uses no axioms

Assumes

CommSemiringCommSemiringAddCommMonoidAlgebraModuleModule