Theorems · Theorem · commutative algebra

Derivation.leibniz_of_mul_eq_one

∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module A M] [inst_5 : Module R M] (D : Derivation R A M) {a b : A},
  a * b = 1 → D a = -a ^ 2 • D b

Defined in

Mathlib.RingTheory.Derivation.Basic

Cited by

4 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext, Quot.sound

Assumes

CommRingCommRingAlgebraAddCommGroupModuleModule