Theorems · Theorem · commutative algebra

DualNumber.lift_apply_inl

∀ {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), (DualNumber.lift fe) (TrivSqZeroExt.inl a) = (↑fe).1 a

When applied to inl, DualNumber.lift applies the map f : A →ₐ[R] B.

Defined in

Mathlib.Algebra.DualNumber

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringSemiringAlgebraAlgebra