Theorems · Theorem · commutative algebra

DualNumber.lift_smul

∀ {R : Type u_1} {B : Type u_3} {A : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (fe : { _fe // _fe.2 * _fe.2 = 0 ∧ ∀ (a : A), Commute _fe.2 (_fe.1 a) })
  (a : A) (ad : DualNumber A), (DualNumber.lift fe) (a • ad) = (↑fe).1 a * (DualNumber.lift fe) ad

Scaling on the left is sent by DualNumber.lift to multiplication on the left

Defined in

Mathlib.Algebra.DualNumber

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringSemiringAlgebraAlgebra