English
Given an alternating map f: M1 [⋀^ι]→ₗ[R] R and z ∈ M2, the smulRight construction corresponds to the multilinear map smulRight: (f.smulRight z)(v) = f(v) • z.
Русский
Для f: M1 [⋀^ι]→ₗ[R] R и z ∈ M2 операция smulRight совпадает с обычным умножением на z: (f.smulRight z)(v) = f(v) • z.
LaTeX
$$$ (f.\mathrm{smulRight} z)(v) = f(v) \cdot z. $$$
Lean4
/-- Given an alternating `R`-multilinear map `f` taking values in `R`, `f.smul_right z` is the map
sending `m` to `f m • z`. -/
@[simps!]
def smulRight {R M₁ M₂ ι : Type*} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂]
(f : M₁ [⋀^ι]→ₗ[R] R) (z : M₂) : M₁ [⋀^ι]→ₗ[R] M₂ :=
{ f.toMultilinearMap.smulRight z with map_eq_zero_of_eq' := fun v i j h hne => by simp [f.map_eq_zero_of_eq v h hne] }
