mul_scalar_mul — Mathlib

English

A scalar holor of dimension 0 acts on a holor by scalar multiplication: x ⊗ y = x • y when x is a scalar holor.

Русский

Холор нулевой размерности действует на холор скалярным умножением: x ⊗ y = x • y, если x — скалярный холор.

LaTeX

$$$[Mul\, \alpha]\ (x:\ Holor\, \alpha\ [])\ (y:\ Holor\, \alpha\ ds) : x \otimes y = x \langle [], \mathbf{nil}\rangle \cdot y$$$

Lean4

theorem mul_scalar_mul [Mul α] (x : Holor α []) (y : Holor α ds) : x ⊗ y = x ⟨[], Forall₂.nil⟩ • y := by
  simp +unfoldPartialApp [mul, SMul.smul, HolorIndex.take, HolorIndex.drop, HSMul.hSMul]
    -- holor slices

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