Theorems · Theorem · commutative algebra

Module.End.exp_mul_of_derivation

∀ (R : Type u_4) (B : Type u_5) [inst : CommRing R] [inst_1 : NonUnitalNonAssocRing B] [inst_2 : Module R B]
  [SMulCommClass R B B] [IsScalarTower R B B] [inst_5 : Module ℚ B] (D : B →ₗ[R] B),
  (∀ (x y : B), D (x * y) = x * D y + D x * y) →
    IsNilpotent D → ∀ (x y : B), (IsNilpotent.exp D) (x * y) = (IsNilpotent.exp D) x * (IsNilpotent.exp D) y

Defined in

Mathlib.RingTheory.Nilpotent.Exp

Cited by

0 results in Mathlib

Foundations

Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingNonUnitalNonAssocRingModuleSMulCommClassIsScalarTowerModule