smulRight — Mathlib

English

For a continuous R-alternating map f taking values in R, the right-scalar multiplication by z ∈ N yields a continuous alternating map f.smulRight z: m ↦ f(m) · z.

Русский

Для непрерывного R-альтернирующего отображения f, принимающего значения в R, умножение справа на элемент z ∈ N даёт непрерывное чередующее отображение f.smulRight z: m ↦ f(m) · z.

LaTeX

$$$$ (f.smulRight z)(m) = f(m) \\cdot z. $$$$

Lean4

/-- Given a continuous `R`-alternating map `f` taking values in `R`, `f.smulRight z` is the
continuous alternating map sending `m` to `f m • z`. -/
@[simps! toContinuousMultilinearMap apply]
def smulRight : M [⋀^ι]→L[R] N :=
  { f.toAlternatingMap.smulRight z with toContinuousMultilinearMap := f.1.smulRight z }

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