lift_op_smul — Mathlib

English

Right scalar action of a on ad corresponds to multiplying the lifted result by f(a) on the right.

Русский

Правое действие на ε соответствует умножению на f(a) справа.

LaTeX

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

Lean4

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

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