lift_smul — Mathlib

English

Left multiplication by an element a in A translates to multiplication by f(a) on the lifted result.

Русский

Левое умножение на элемент a в A переводится в умножение на f(a) на лифтовом результате.

LaTeX

$$$\text{lift } fe (a \cdot ad) = fe.1 a \cdot (\text{lift } fe\; ad)$$$

Lean4

/-- Scaling on the left is sent by `DualNumber.lift` to multiplication on the left -/
@[simp]
theorem lift_smul (fe : { _fe : (A →ₐ[R] B) × B // _ }) (a : A) (ad : A[ε]) :
    lift fe (a • ad) = fe.val.1 a * lift fe ad := by rw [← inl_mul_eq_smul, map_mul, lift_apply_inl]

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