lift_apply_inl — Mathlib

English

The lift respects the base algebra map on pure base elements.

Русский

Лифт сохраняет осн. отображение на чистых элементах базы.

LaTeX

$$$(\text{lift } fe)(\text{inl } a) = fe.1 a,$$$

Lean4

/-- When applied to `inl`, `DualNumber.lift` applies the map `f : A →ₐ[R] B`. -/
@[simp]
theorem lift_apply_inl (fe : { _fe : (A →ₐ[R] B) × B // _ }) (a : A) : lift fe (inl a : A[ε]) = fe.val.1 a := by
  rw [lift_apply_apply, fst_inl, snd_inl, map_zero, zero_mul, add_zero]

Похожие утверждения