coe_smulRight — Mathlib

English

The simplification lemma: coercion commutes with smulRight in the target.

Русский

Лемма упрощения: приведение к типу и smulRight совместимы в цели.

LaTeX

$$$ (f.smulRight z) = f.smulRight z. $$$

Lean4

@[simp]
theorem coe_smulRight {R M₁ M₂ ι : Type*} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁]
    [Module R M₂] (f : M₁ [⋀^ι]→ₗ[R] R) (z : M₂) :
    (f.smulRight z : MultilinearMap R (fun _ : ι => M₁) M₂) = MultilinearMap.smulRight f z :=
  rfl

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